1  /-
  2  Copyright (c) 2015 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Leonardo de Moura, Mario Carneiro
  5  
  6  In the standard library we cannot assume the univalence axiom.
  7  We say two types are equivalent if they are isomorphic.
  8  
  9  Two equivalent types have the same cardinality.
 10  -/
 11  import tactic.split_ifs logic.function logic.unique data.set.function data.bool data.quot
src         └──────────────┘ └────────────┘ └──────────┘ └───────────────┘ └───────┘ └───────┘
 12  
 13  open function
 14  
 15  universes u v w
 16  variables {α : Sort u} {β : Sort v} {γ : Sort w}
 17  
 18  /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
 19  structure equiv (α : Sort*) (β : Sort*) :=
id                        └───┘       └───┘
typ                       └───┘       └───┘
 20  (to_fun    : α → β)
id                  
typ                 
 21  (inv_fun   : β → α)
id                  
typ                 
 22  (left_inv  : left_inverse inv_fun to_fun)
id                └──────────┘ └─────┘ └────┘
src               └──────────┘
typ               └──────────┘ └─────┘ └────┘
 23  (right_inv : right_inverse inv_fun to_fun)
id                └───────────┘ └─────┘ └────┘
src               └───────────┘
typ               └───────────┘ └─────┘ └────┘
 24  
 25  infix ` ≃ `:25 := equiv
id                     └───┘
src                    └───┘
typ                    └───┘
doc                    └───┘
 26  
 27  def function.involutive.to_equiv {f : α → α} (h : involutive f) : α ≃ α :=
id                                                   └────────┘       
src                                                    └────────┘        
typ                                                  └────────┘       
doc                                                    └────────┘        
 28  ⟨f, f, h.left_inverse, h.right_inverse⟩
id        └───────────┘  └────────────┘
src          └───────────┘   └────────────┘
typ       └───────────┘  └────────────┘
 29  
 30  namespace equiv
 31  
 32  /-- `perm α` is the type of bijections from `α` to itself. -/
 33  @[reducible] def perm (α : Sort*) := equiv α α
id                                        └───┘  
src                                       └───┘
typ                                       └───┘  
doc    └───────┘                          └───┘
 34  
 35  instance : has_coe_to_fun (α ≃ β) :=
id              └────────────┘    
src             └────────────┘    
typ             └────────────┘    
doc                               
 36  ⟨_, to_fun⟩
id       └────┘
src      └────┘
typ      └────┘
 37  
 38  @[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
id                                                  └──────┘             
src                                                   └──────┘                  
typ                                                 └──────┘             
doc    └──┘
 39  rfl
id   └─┘
src  └─┘
typ  └─┘
 40  
 41  theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : equiv α β}, (e₁ : α → β) = e₂ → e₁ = e₂
id                                       └───┘      └┘         └┘   └┘  └┘
src                                       └───┘                             
typ                                      └───┘      └┘         └┘   └┘  └┘
doc                                       └───┘
 42  | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ h :=
id      └┘  └┘  └┘  └┘   └┘  └┘      └┘  
typ     └┘  └┘  └┘  └┘   └┘  └┘      └┘  
 43    have f₁ = f₂, from h,
id             
src            
typ            
 44    have g₁ = g₂, from funext $ assume x,
id                       └────┘          
src                      └────┘
typ                      └────┘          
 45      have f₁ (g₁ x) = f₂ (g₂ x), from (r₁ x).trans (r₂ x).symm,
id                                          └───┘       └──┘
src                                            └───┘        └──┘
typ                                         └───┘       └──┘
 46      have f₁ (g₁ x) = f₁ (g₂ x), by { subst f₂, exact this },
id                                           └┘        └──┘
src                                      └────┘    └────┘    
typ                                    └────┘└┘  └────┘└──┘
doc                                       └────┘    └────┘    
txt                                       └────┘    └────┘    
par                                       └────┘    └────┘    
pid                                                         
st                                     └─────────┘└───────────┘└┘
 47      show g₁ x = g₂ x,           from injective_of_left_inverse l₁ this,
id                                     └───────────────────────┘    └──┘
src                                      └───────────────────────┘
typ                                    └───────────────────────┘    └──┘
 48    by simp *
src       └──────
typ       └──────
doc       └──────
txt       └──────
par       └──────
pid           
st       └───────
 49  
src  
typ  
doc  
txt  
par  
pid  
st   
 50  @[ext] lemma ext (f g : equiv α β) (H : ∀ x, f x = g x) : f = g :=
id                           └───┘                       
src                          └───┘                              
typ                          └───┘                       
doc    └─┘                   └───┘
 51  eq_of_to_fun_eq (funext H)
id   └─────────────┘  └────┘ 
src  └─────────────┘  └────┘
typ  └─────────────┘  └────┘ 
 52  
 53  @[ext] lemma perm.ext (σ τ : equiv.perm α) (H : ∀ x, σ x = τ x) : σ = τ :=
id                                └────────┘                      
src                               └────────┘                            
typ                               └────────┘                      
doc    └─┘                        └────────┘
 54  equiv.ext _ _ H
id   └───────┘     
src  └───────┘
typ  └───────┘     
 55  
 56  @[refl] protected def refl (α : Sort*) : α ≃ α := ⟨id, id, λ x, rfl, λ x, rfl⟩
id                                                   └┘  └┘      └─┘      └─┘
src    └──┘                                            └┘  └┘       └─┘       └─┘
typ                                                  └┘  └┘      └─┘      └─┘
doc    └──┘                                     
 57  
 58  @[symm] protected def symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
id                                                └──────┘  └─────┘  └────────┘  └───────┘
src    └──┘                                            └──────┘   └─────┘   └────────┘   └───────┘
typ                                               └──────┘  └─────┘  └────────┘  └───────┘
doc    └──┘                                    
 59  
 60  @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
id                                                        
src    └───┘                                                  
typ                                                       
doc    └───┘                                                  
 61  ⟨e₂.to_fun ∘ e₁.to_fun, e₁.inv_fun ∘ e₂.inv_fun,
id    └┘└─────┘  └┘└─────┘  └┘└──────┘  └┘└──────┘
src     └─────┘    └─────┘    └──────┘    └──────┘
typ   └┘└─────┘  └┘└─────┘  └┘└──────┘  └┘└──────┘
 62    e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
id     └┘└───────┘└───┘ └┘└───────┘  └┘└────────┘└───┘ └┘└────────┘
src      └───────┘└───┘   └───────┘    └────────┘└───┘   └────────┘
typ    └┘└───────┘└───┘ └┘└───────┘  └┘└────────┘└───┘ └┘└────────┘
 63  
 64  protected theorem injective : ∀ f : α ≃ β, injective f
id                                          └───────┘ 
src                                            └───────┘
typ                                         └───────┘ 
doc                                        
 65  | ⟨f, g, h₁, h₂⟩ := injective_of_left_inverse h₁
id            └┘         └───────────────────────┘
src                      └───────────────────────┘
typ           └┘         └───────────────────────┘
 66  
 67  protected theorem surjective : ∀ f : α ≃ β, surjective f
id                                           └────────┘ 
src                                             └────────┘
typ                                          └────────┘ 
doc                                         
 68  | ⟨f, g, h₁, h₂⟩ := surjective_of_has_right_inverse ⟨_, h₂⟩
id                └┘     └─────────────────────────────┘
src                      └─────────────────────────────┘
typ               └┘     └─────────────────────────────┘
 69  
 70  protected theorem bijective (f : α ≃ β) : bijective f :=
id                                          └───────┘ 
src                                           └───────┘
typ                                         └───────┘ 
doc                                     
 71  ⟨f.injective, f.surjective⟩
id    └────────┘  └─────────┘
src    └────────┘   └─────────┘
typ   └────────┘  └─────────┘
 72  
 73  @[simp] lemma range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) : set.range e = set.univ :=
id                                                                  └───────┘   └──────┘
src                                                                   └───────┘    └──────┘
typ                                                                 └───────┘   └──────┘
doc    └──┘                                                           └───────┘
 74  set.eq_univ_of_forall e.surjective
id   └───────────────────┘ └─────────┘
src  └───────────────────┘  └─────────┘
typ  └───────────────────┘ └─────────┘
 75  
 76  protected theorem subsingleton (e : α ≃ β) : ∀ [subsingleton β], subsingleton α
id                                               └───────────┘    └──────────┘ 
src                                                └───────────┘     └──────────┘
typ                                              └──────────┘    └──────────┘ 
doc                                        
 77  | ⟨H⟩ := ⟨λ a b, e.injective (H _ _)⟩
id                 └────────┘
src                    └────────┘
typ                └────────┘
 78  
 79  protected def decidable_eq (e : α ≃ β) [H : decidable_eq β] : decidable_eq α
id                                            └──────────┘     └──────────┘ 
src                                             └──────────┘      └──────────┘
typ                                           └──────────┘     └──────────┘ 
doc                                    
 80  | a b := decidable_of_iff _ e.injective.eq_iff
id            └──────────────┘   └────────┘└─────┘
src           └──────────────┘    └────────┘└─────┘
typ           └──────────────┘   └────────┘└─────┘
 81  
 82  lemma nonempty_iff_nonempty : α ≃ β → (nonempty α ↔ nonempty β)
id                                      └──────┘   └──────┘ 
src                                        └──────┘    └──────┘
typ                                     └──────┘   └──────┘ 
doc                                  
 83  | ⟨f, g, _, _⟩ := nonempty.congr f g
id                   └────────────┘
src                    └────────────┘
typ                  └────────────┘
 84  
 85  protected def cast {α β : Sort*} (h : α = β) : α ≃ β :=
id                                                 
src                                                  
typ                                                
doc                                                   
 86  ⟨cast h, cast h.symm, λ x, by { cases h, refl }, λ x, by { cases h, refl }⟩
id    └──┘   └──┘ └───┘                                          
src   └──┘    └──┘  └───┘            └────┘   └───┘             └────┘   └───┘
typ   └──┘   └──┘ └───┘           └────┘  └───┘            └────┘  └───┘
doc                                  └────┘   └───┘             └────┘   └───┘
txt                                  └────┘   └───┘             └────┘   └───┘
par                                  └────┘   └───┘             └────┘   └───┘
pid                                                                       
st                                └────────┘└─────┘└┘        └────────┘└─────┘└┘
 87  
 88  @[simp] theorem coe_fn_symm_mk (f : α → β) (g l r) : ((equiv.mk f g l r).symm : β → α) = g :=
id                                                        └──────┘     └──┘          
src                                                         └──────┘         └──┘           
typ                                                       └──────┘     └──┘          
doc    └──┘
 89  rfl
id   └─┘
src  └─┘
typ  └─┘
 90  
 91  @[simp] theorem refl_apply (x : α) : equiv.refl α x = x := rfl
id                                       └────────┘        └─┘
src                                       └────────┘           └─┘
typ                                      └────────┘        └─┘
doc    └──┘
 92  
 93  @[simp] theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl
id                                                           └────┘             └─┘
src                                                                └────┘                  └─┘
typ                                                          └────┘             └─┘
doc    └──┘                                        
 94  
 95  @[simp] theorem apply_symm_apply : ∀ (e : α ≃ β) (x : β), e (e.symm x) = x
id                                                          └───┘    
src                                                               └───┘    
typ                                                         └───┘    
doc    └──┘                                      
 96  | ⟨f₁, g₁, l₁, r₁⟩ x := by { simp [equiv.symm], rw r₁ }
id                  └┘                  └────────┘      └┘
src                               └────┘└────────┘  └─┘  
typ                 └┘            └────┘└────────┘  └─┘└┘
doc                               └────┘            └─┘  
txt                               └────┘            └─┘  
par                               └────┘            └─┘  
pid                                                   
st                             └──────────────────┘└──────┘└┘
 97  
 98  @[simp] theorem symm_apply_apply : ∀ (e : α ≃ β) (x : α), e.symm (e x) = x
id                                                        └───┘      
src                                                            └───┘       
typ                                                       └───┘      
doc    └──┘                                      
 99  | ⟨f₁, g₁, l₁, r₁⟩ x := by { simp [equiv.symm], rw l₁ }
id              └┘                      └────────┘      └┘
src                               └────┘└────────┘  └─┘  
typ             └┘                └────┘└────────┘  └─┘└┘
doc                               └────┘            └─┘  
txt                               └────┘            └─┘  
par                               └────┘            └─┘  
pid                                                   
st                             └──────────────────┘└──────┘└┘
100  
101  @[simp] lemma symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
id                                                         
src                                                   
typ                                                        
doc    └──┘                                           
102    (f.trans g).symm a = f.symm (g.symm a) := rfl
id      └────┘  └──┘    └───┘  └───┘      └─┘
src      └────┘   └──┘      └───┘   └───┘       └─┘
typ     └────┘  └──┘    └───┘  └───┘      └─┘
103  
104  @[simp] theorem apply_eq_iff_eq : ∀ (f : α ≃ β) (x y : α), f x = f y ↔ x = y
id                                                                 
src                                                                        
typ                                                                
doc    └──┘                                     
105  | ⟨f₁, g₁, l₁, r₁⟩ x y := (injective_of_left_inverse l₁).eq_iff
id              └┘              └───────────────────────┘    └────┘
src                             └───────────────────────┘    └────┘
typ             └┘              └───────────────────────┘    └────┘
106  
107  @[simp] theorem cast_apply {α β} (h : α = β) (x : α) : equiv.cast h x = cast h x := rfl
id                                                      └────────┘    └──┘      └─┘
src                                                        └────────┘      └──┘        └─┘
typ                                                     └────────┘    └──┘      └─┘
doc    └──┘
108  
109  lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
id                                              └───┘        
src                                                └───┘         
typ                                             └───┘        
doc                                   
110  ⟨λ H, by simp [H.symm], λ H, by simp [H]⟩
id                                       
src           └────┘                └────┘ 
typ          └────┘└────┘         └────┘
doc           └────┘                └────┘ 
txt           └────┘                └────┘ 
par           └────┘                └────┘ 
pid                                    
st           └────────────┘         └───────┘
111  
112  lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
id                                                └───┘      
src                                                   └───┘        
typ                                               └───┘      
doc                                   
113  (eq_comm.trans e.symm_apply_eq).trans eq_comm
id    └─────┘└────┘ └────────────┘ └───┘  └─────┘
src   └─────┘└────┘  └────────────┘ └───┘  └─────┘
typ   └─────┘└────┘ └────────────┘ └───┘  └─────┘
114  
115  @[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
id                                        └────────┘                 
src                                          └────────┘            └────┘   └───┘
typ                                       └───┘└───┘           └────┘  └───┘
doc    └──┘                                                         └────┘   └───┘
txt                                                                  └────┘   └───┘
par                                                                  └────┘   └───┘
pid                                                                              
st                                                                └────────┘└─────┘└┘
116  
117  @[simp] theorem symm_symm_apply (e : α ≃ β) (a : α) : e.symm.symm a = e a := by { cases e, refl }
id                                                     └────────┘                   
src                                                        └────────┘                └────┘   └───┘
typ                                                    └───┘└───┘             └────┘  └───┘
doc    └──┘                                                                           └────┘   └───┘
txt                                                                                    └────┘   └───┘
par                                                                                    └────┘   └───┘
pid                                                                                                
st                                                                                  └────────┘└─────┘└┘
118  
119  @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl }
id                                         └────┘  └────────┘                   
src                                           └────┘  └────────┘               └────┘   └───┘
typ                                        └────┘  └────────┘             └────┘  └───┘
doc    └──┘                                                                     └────┘   └───┘
txt                                                                              └────┘   └───┘
par                                                                              └────┘   └───┘
pid                                                                                          
st                                                                            └────────┘└─────┘└┘
120  
121  @[simp] theorem refl_symm : (equiv.refl α).symm = equiv.refl α := rfl
id                                └────────┘  └──┘   └────────┘     └─┘
src                               └────────┘   └──┘   └────────┘      └─┘
typ                               └────────┘  └──┘   └────────┘     └─┘
doc    └──┘
122  
123  @[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }
id                                          └────────┘  └───┘                   
src                                           └────────┘   └───┘               └────┘   └───┘
typ                                         └────────┘  └───┘             └────┘  └───┘
doc    └──┘                                                                     └────┘   └───┘
txt                                                                              └────┘   └───┘
par                                                                              └────┘   └───┘
pid                                                                                          
st                                                                            └────────┘└─────┘└┘
124  
125  @[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β :=  ext _ _ (by simp)
id                                         └───┘└────┘   └────────┘      └─┘
src                                           └───┘└────┘    └────────┘       └─┘         └──┘
typ                                        └───┘└────┘   └────────┘      └─┘         └──┘
doc    └──┘                                                                                └──┘
txt                                                                                         └──┘
par                                                                                         └──┘
st                                                                                         └───┘
126  
127  @[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext _ _ (by simp)
id                                         └────┘ └───┘  └────────┘     └─┘
src                                           └────┘  └───┘  └────────┘      └─┘         └──┘
typ                                        └────┘ └───┘  └────────┘     └─┘         └──┘
doc    └──┘                                                                               └──┘
txt                                                                                        └──┘
par                                                                                        └──┘
st                                                                                        └───┘
128  
129  lemma trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
id                                                     
src                                                        
typ                                                    
doc                                                        
130    (ab.trans bc).trans cd = ab.trans (bc.trans cd) :=
id      └┘└────┘ └┘ └───┘  └┘  └┘└────┘  └┘└────┘ └┘
src       └────┘    └───┘        └────┘    └────┘
typ     └┘└────┘ └┘ └───┘  └┘  └┘└────┘  └┘└────┘ └┘
131  equiv.ext _ _ $ assume a, rfl
id   └───────┘                └─┘
src  └───────┘                 └─┘
typ  └───────┘                └─┘
132  
133  theorem left_inverse_symm (f : equiv α β) : left_inverse f.symm f := f.left_inv
id                                  └───┘      └──────────┘ └───┘     └───────┘
src                                 └───┘        └──────────┘  └───┘       └───────┘
typ                                 └───┘      └──────────┘ └───┘     └───────┘
doc                                 └───┘
134  
135  theorem right_inverse_symm (f : equiv α β) : function.right_inverse f.symm f := f.right_inv
id                                   └───┘      └────────────────────┘ └───┘     └────────┘
src                                  └───┘        └────────────────────┘  └───┘       └────────┘
typ                                  └───┘      └────────────────────┘ └───┘     └────────┘
doc                                  └───┘
136  
137  def equiv_congr {δ} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ) :=
id                                                      
src                                                           
typ                                                     
doc                                                           
138  ⟨ λac, (ab.symm.trans ac).trans cd, λbd, ab.trans $ bd.trans $ cd.symm,
id      └┘   └┘└───┘└────┘ └┘ └───┘  └┘   └┘  └┘└────┘   └┘└────┘   └┘└───┘
src            └───┘└────┘    └───┘             └────┘     └────┘     └───┘
typ     └┘   └┘└───┘└────┘ └┘ └───┘  └┘   └┘  └┘└────┘   └┘└────┘   └┘└───┘
139    assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end,
id            └┘              └─────────┘         └─────────┘
src                     └────┘└─────────┘  └────┘└─────────┘  └───┘
typ           └┘        └────┘└─────────┘  └────┘└─────────┘  └───┘
doc                     └────┘             └────┘             └───┘
txt                     └────┘             └────┘             └───┘
par                     └────┘             └────┘             └───┘
pid                                        └──┘                 
st                └──────────────────────┘└─────────────────┘└──────┘└─┘
140    assume ac, begin simp [trans_assoc], rw [← trans_assoc], simp end, ⟩
id            └┘              └─────────┘         └─────────┘
src                     └────┘└─────────┘  └────┘└─────────┘  └───┘
typ           └┘        └────┘└─────────┘  └────┘└─────────┘  └───┘
doc                     └────┘             └────┘             └───┘
txt                     └────┘             └────┘             └───┘
par                     └────┘             └────┘             └───┘
pid                                        └──┘                 
st                └──────────────────────┘└─────────────────┘└──────┘└─┘
141  
142  def perm_congr {α : Type*} {β : Type*} (e : α ≃ β) : perm α ≃ perm β :=
id                                                     └──┘   └──┘ 
src                                                      └──┘    └──┘
typ                                                    └──┘   └──┘ 
doc                                                      └──┘    └──┘
143  equiv_congr e e
id   └─────────┘  
src  └─────────┘
typ  └─────────┘  
144  
145  protected lemma image_eq_preimage {α β} (e : α ≃ β) (s : set α) : e '' s = e.symm ⁻¹' s :=
id                                                         └─┘      └┘   └───┘ └─┘ 
src                                                          └─┘        └┘     └───┘ └─┘
typ                                                        └─┘      └┘   └───┘ └─┘ 
doc                                                                                   └─┘
146  set.ext $ assume x, set.mem_image_iff_of_inverse e.left_inv e.right_inv
id   └─────┘            └──────────────────────────┘ └───────┘ └────────┘
src  └─────┘             └──────────────────────────┘  └───────┘  └────────┘
typ  └─────┘            └──────────────────────────┘ └───────┘ └────────┘
147  
148  protected lemma subset_image {α β} (e : α ≃ β) (s : set α) (t : set β) : t ⊆ e '' s ↔ e.symm '' t ⊆ s :=
id                                                    └─┘        └─┘        └┘   └───┘ └┘   
src                                                     └─┘         └─┘           └┘     └───┘ └┘   
typ                                                   └─┘        └─┘        └┘   └───┘ └┘   
doc                                            
149  by rw [set.image_subset_iff, e.image_eq_preimage]
id          └──────────────────┘
src     └──┘└──────────────────┘└┘                   └─
typ     └──┘└──────────────────┘└┘└─────────────────┘└─
doc     └──┘└──────────────────┘└┘                   └─
txt     └──┘                    └┘                   └─
par     └──┘                    └┘                   └─
pid       └┘                    └┘                   
st     └───────────────────────┘└───────────────────┘
150  
src  
typ  
doc  
txt  
par  
pid  
st   
151  lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f '' s) = s :=
id                                     └───┘         └─┘     └───┘ └┘   └┘    
src                                    └───┘           └─┘       └───┘ └┘    └┘    
typ                                    └───┘         └─┘     └───┘ └┘   └┘    
doc                                    └───┘
152  by { rw [← set.image_comp], simp }
id              └────────────┘
src       └────┘└────────────┘  └───┘
typ       └────┘└────────────┘  └───┘
doc       └────┘                └───┘
txt       └────┘                └───┘
par       └────┘                └───┘
pid         └──┘                    
st     └─────────────────────┘└──────┘└┘
153  
154  protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
id                                          └───┘         └─┘ 
src                                         └───┘           └─┘
typ                                         └───┘         └─┘ 
doc                                         └───┘
155    f '' -s = -(f '' s) :=
id      └┘     └┘ 
src      └┘       └┘
typ     └┘     └┘ 
156  set.image_compl_eq f.bijective
id   └────────────────┘ └────────┘
src  └────────────────┘  └────────┘
typ  └────────────────┘ └────────┘
157  
158  /- The group of permutations (self-equivalences) of a type `α` -/
159  
160  namespace perm
161  
162  instance perm_group {α : Type u} : group (perm α) :=
id                                      └───┘  └──┘ 
src                                     └───┘  └──┘
typ                                     └───┘  └──┘ 
doc                                            └──┘
163  begin
st   └─────
164    refine { mul := λ f g, equiv.trans g f, one := equiv.refl α, inv:= equiv.symm, ..};
id                            └─────────┘             └────────┘         └────────┘
src    └─────┘ └──────┘ └────┘└─────────┘  └───────┘└────────┘ └──────┘└────────┘└───┘
typ    └─────┘ └──────┘ └────┘└─────────┘  └───────┘└────────┘└──────┘└────────┘└───┘
doc    └─────┘ └──────┘ └────┘             └───────┘           └──────┘          └───┘
txt    └─────┘ └──────┘ └────┘             └───────┘           └──────┘          └───┘
par    └─────┘ └──────┘ └────┘             └───────┘           └──────┘          └───┘
pid           └──────┘ └────┘             └───────┘           └──────┘          └───┘
st   ──────────────────────────────────────────────────────────────────────────────────────
165    intros; apply equiv.ext; try { apply trans_apply },
id                   └───────┘              └─────────┘
src    └────┘  └────┘└───────┘  └────┘└────┘└─────────┘
typ    └────┘  └────┘└───────┘  └────┘└────┘└─────────┘
doc    └────┘  └────┘           └────┘└────┘           
txt    └────┘  └────┘           └────┘└────┘           
par    └────┘  └────┘           └────┘└────┘           
pid                               └───────┘           └┘
st   ───────────────────────────────┘└─────────────────┘└┘
166    apply symm_apply_apply
id           └──────────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ────────────────────────┘
167  end
st   └─┘
168  
169  @[simp] theorem mul_apply {α : Type u} (f g : perm α) (x) : (f * g) x = f (g x) :=
id                                                 └──┘                   
src                                                └──┘                   
typ                                                └──┘                   
doc    └──┘                                        └──┘
170  equiv.trans_apply _ _ _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
171  
172  @[simp] theorem one_apply {α : Type u} (x) : (1 : perm α) x = x := rfl
id                                                     └──┘         └─┘
src                                                    └──┘            └─┘
typ                                                    └──┘         └─┘
doc    └──┘                                            └──┘
173  
174  @[simp] lemma inv_apply_self {α : Type u} (f : perm α) (x) :
id                                                  └──┘ 
src                                                 └──┘
typ                                                 └──┘ 
doc    └──┘                                         └──┘
175    f⁻¹ (f x) = x := equiv.symm_apply_apply _ _
id     └┘          └────────────────────┘
src     └┘             └────────────────────┘
typ    └┘          └────────────────────┘
176  
177  @[simp] lemma apply_inv_self {α : Type u} (f : perm α) (x) :
id                                                  └──┘ 
src                                                 └──┘
typ                                                 └──┘ 
doc    └──┘                                         └──┘
178    f (f⁻¹ x) = x := equiv.apply_symm_apply _ _
id       └┘        └────────────────────┘
src        └┘          └────────────────────┘
typ      └┘        └────────────────────┘
179  
180  lemma one_def {α : Type u} : (1 : perm α) = equiv.refl α := rfl
id                                     └──┘    └────────┘     └─┘
src                                    └──┘     └────────┘      └─┘
typ                                    └──┘    └────────┘     └─┘
doc                                    └──┘
181  
182  lemma mul_def {α : Type u} (f g : perm α) : f * g = g.trans f := rfl
id                                     └──┘         └────┘     └─┘
src                                    └──┘             └────┘      └─┘
typ                                    └──┘         └────┘     └─┘
doc                                    └──┘
183  
184  lemma inv_def {α : Type u} (f : perm α) : f⁻¹ = f.symm := rfl
id                                   └──┘     └┘  └───┘    └─┘
src                                  └──┘       └┘   └───┘    └─┘
typ                                  └──┘     └┘  └───┘    └─┘
doc                                  └──┘
185  
186  end perm
187  
188  def equiv_empty (h : α → false) : α ≃ empty :=
id                           └───┘      └───┘
src                           └───┘       └───┘
typ                          └───┘      └───┘
doc                                      
189  ⟨λ x, (h x).elim, λ e, e.rec _, λ x, (h x).elim, λ e, e.rec _⟩
id           └──┘       └──┘           └──┘       └──┘
src             └──┘         └──┘              └──┘         └──┘
typ          └──┘       └──┘           └──┘       └──┘
190  
191  def false_equiv_empty : false ≃ empty :=
id                           └───┘  └───┘
src                          └───┘  └───┘
typ                          └───┘  └───┘
doc                                
192  equiv_empty _root_.id
id   └─────────┘ └───────┘
src  └─────────┘ └───────┘
typ  └─────────┘ └───────┘
193  
194  def equiv_pempty (h : α → false) : α ≃ pempty :=
id                            └───┘      └────┘
src                            └───┘       └────┘
typ                           └───┘      └────┘
doc                                        └────┘
195  ⟨λ x, (h x).elim, λ e, e.rec _, λ x, (h x).elim, λ e, e.rec _⟩
id           └──┘       └──┘           └──┘       └──┘
src             └──┘         └──┘              └──┘         └──┘
typ          └──┘       └──┘           └──┘       └──┘
196  
197  def false_equiv_pempty : false ≃ pempty :=
id                            └───┘  └────┘
src                           └───┘  └────┘
typ                           └───┘  └────┘
doc                                  └────┘
198  equiv_pempty _root_.id
id   └──────────┘ └───────┘
src  └──────────┘ └───────┘
typ  └──────────┘ └───────┘
199  
200  def empty_equiv_pempty : empty ≃ pempty :=
id                            └───┘  └────┘
src                           └───┘  └────┘
typ                           └───┘  └────┘
doc                                  └────┘
201  equiv_pempty $ empty.rec _
id   └──────────┘   └───────┘
src  └──────────┘   └───────┘
typ  └──────────┘   └───────┘
202  
203  def pempty_equiv_pempty : pempty.{v} ≃ pempty.{w} :=
id                             └────┘      └────┘
src                            └────┘      └────┘
typ                            └────┘      └────┘
doc                            └────┘      └────┘
204  equiv_pempty pempty.elim
id   └──────────┘ └─────────┘
src  └──────────┘ └─────────┘
typ  └──────────┘ └─────────┘
205  
206  def empty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ empty :=
id                                               └──────┘       └───┘
src                                              └──────┘         └───┘
typ                                              └──────┘       └───┘
doc                                                               
207  equiv_empty $ assume a, h ⟨a⟩
id   └─────────┘              
src  └─────────┘
typ  └─────────┘              
208  
209  def pempty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ pempty :=
id                                                └──────┘       └────┘
src                                               └──────┘         └────┘
typ                                               └──────┘       └────┘
doc                                                                 └────┘
210  equiv_pempty $ assume a, h ⟨a⟩
id   └──────────┘              
src  └──────────┘
typ  └──────────┘              
211  
212  def prop_equiv_punit {p : Prop} (h : p) : p ≃ punit :=
id                                              └───┘
src                                               └───┘
typ                                             └───┘
doc                                              
213  ⟨λ x, (), λ x, h, λ _, rfl, λ ⟨⟩, rfl⟩
id        └┘            └─┘       └─┘
src        └┘               └─┘       └─┘
typ       └┘            └─┘       └─┘
214  
215  def true_equiv_punit : true ≃ punit := prop_equiv_punit trivial
id                          └──┘  └───┘    └──────────────┘ └─────┘
src                         └──┘  └───┘    └──────────────┘ └─────┘
typ                         └──┘  └───┘    └──────────────┘ └─────┘
doc                              
216  
217  protected def ulift {α : Type u} : ulift α ≃ α :=
id                                      └───┘   
src                                     └───┘   
typ                                     └───┘   
doc                                     └───┘   
218  ⟨ulift.down, ulift.up, ulift.up_down, λ a, rfl⟩
id    └────────┘  └──────┘  └───────────┘      └─┘
src   └────────┘  └──────┘  └───────────┘       └─┘
typ   └────────┘  └──────┘  └───────────┘      └─┘
219  
220  protected def plift : plift α ≃ α :=
id                         └───┘   
src                        └───┘   
typ                        └───┘   
doc                        └───┘   
221  ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩
id    └────────┘  └──────┘  └───────────┘  └───────────┘
src   └────────┘  └──────┘  └───────────┘  └───────────┘
typ   └────────┘  └──────┘  └───────────┘  └───────────┘
222  
223  @[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
id                                                        └┘  └┘        └┘  └┘
src    └───┘                                                               
typ                                                       └┘  └┘        └┘  └┘
doc    └───┘                                                               
224    (α₁ → β₁) ≃ (α₂ → β₂) :=
id      └┘   └┘    └┘   └┘
src              
typ     └┘   └┘    └┘   └┘
doc              
225  { to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun,
id                   └┘└─────┘    └┘└──────┘
src                     └─────┘       └──────┘
typ                  └┘└─────┘    └┘└──────┘
226    inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun,
id                    └┘└──────┘    └┘└─────┘
src                      └──────┘       └─────┘
typ                   └┘└──────┘    └┘└─────┘
227    left_inv := λ f, funext $ λ x, by { dsimp, rw [e₂.left_inv, e₁.left_inv] },
id                     └────┘     
src                     └────┘             └───┘  └──┘           └┘           └┘
typ                    └────┘            └───┘  └──┘└─────────┘└┘└─────────┘└┘
doc                                        └───┘  └──┘           └┘           └┘
txt                                        └───┘  └──┘           └┘           └┘
par                                        └───┘  └──┘           └┘           └┘
pid                                                 └┘           └┘           
st                                      └──────┘└───────────────┘└───────────┘└┘
228    right_inv := λ f, funext $ λ x, by { dsimp, rw [e₂.right_inv, e₁.right_inv] } }
id                      └────┘     
src                      └────┘             └───┘  └──┘            └┘            └┘
typ                     └────┘            └───┘  └──┘└──────────┘└┘└──────────┘└┘
doc                                         └───┘  └──┘            └┘            └┘
txt                                         └───┘  └──┘            └┘            └┘
par                                         └───┘  └──┘            └┘            └┘
pid                                                  └┘            └┘            
st                                       └──────┘└────────────────┘└────────────┘└┘
229  
230  @[simp] lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂)
id                                                               └┘  └┘        └┘  └┘
src                                                                               
typ                                                              └┘  └┘        └┘  └┘
doc    └──┘                                                                       
231    (f : α₁ → β₁) (x : α₂) :
id          └┘   └┘       └┘
typ         └┘   └┘       └┘
232    arrow_congr e₁ e₂ f x = (e₂ $ f $ e₁.symm x) :=
id     └─────────┘ └┘ └┘     └┘      └┘└───┘ 
src    └─────────┘                        └───┘
typ    └─────────┘ └┘ └┘     └┘      └┘└───┘ 
233  rfl
id   └─┘
src  └─┘
typ  └─┘
234  
235  lemma arrow_congr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*}
236    (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
id           └┘  └┘        └┘  └┘        └┘  └┘       └┘   └┘       └┘   └┘
src                                         
typ          └┘  └┘        └┘  └┘        └┘  └┘       └┘   └┘       └┘   └┘
doc                                         
237    arrow_congr ea ec (g ∘ f) = (arrow_congr eb ec g) ∘ (arrow_congr ea eb f) :=
id     └─────────┘ └┘ └┘        └─────────┘ └┘ └┘     └─────────┘ └┘ └┘ 
src    └─────────┘                └─────────┘            └─────────┘
typ    └─────────┘ └┘ └┘        └─────────┘ └┘ └┘     └─────────┘ └┘ └┘ 
238  by { ext, simp only [comp, arrow_congr_apply, eb.symm_apply_apply] }
id                        └──┘  └───────────────┘
src       └─┘  └─────────┘└──┘└┘└───────────────┘└┘                   └┘
typ       └─┘  └─────────┘└──┘└┘└───────────────┘└┘└─────────────────┘└┘
doc       └─┘  └─────────┘    └┘                 └┘                   └┘
txt       └─┘  └─────────┘    └┘                 └┘                   └┘
par       └─┘  └─────────┘    └┘                 └┘                   └┘
pid                └──┘└┘    └┘                 └┘                   
st     └────┘└─────────────────────────────────────────────────────────┘└┘
239  
240  @[simp] lemma arrow_congr_refl {α β : Sort*} :
doc    └──┘
241    arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl
id     └─────────┘  └────────┘    └────────┘    └────────┘          └─┘
src    └─────────┘  └────────┘     └────────┘     └────────┘            └─┘
typ    └─────────┘  └────────┘    └────────┘    └────────┘          └─┘
242  
243  @[simp] lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*}
doc    └──┘
244    (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
id           └┘  └┘         └┘  └┘        └┘  └┘         └┘  └┘
src                                                         
typ          └┘  └┘         └┘  └┘        └┘  └┘         └┘  └┘
doc                                                         
245    arrow_congr (e₁.trans e₂) (e₁'.trans e₂') = (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') :=
id     └─────────┘  └┘└────┘ └┘   └─┘└────┘ └─┘    └─────────┘ └┘ └─┘ └───┘   └─────────┘ └┘ └─┘
src    └─────────┘    └────┘         └────┘        └─────────┘        └───┘   └─────────┘
typ    └─────────┘  └┘└────┘ └┘   └─┘└────┘ └─┘    └─────────┘ └┘ └─┘ └───┘   └─────────┘ └┘ └─┘
246  rfl
id   └─┘
src  └─┘
typ  └─┘
247  
248  @[simp] lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
id                                                              └┘  └┘        └┘  └┘
src                                                                              
typ                                                             └┘  └┘        └┘  └┘
doc    └──┘                                                                      
249    (arrow_congr e₁ e₂).symm = arrow_congr e₁.symm e₂.symm :=
id      └─────────┘ └┘ └┘ └──┘   └─────────┘ └┘└───┘ └┘└───┘
src     └─────────┘       └──┘   └─────────┘   └───┘   └───┘
typ     └─────────┘ └┘ └┘ └──┘   └─────────┘ └┘└───┘ └┘└───┘
250  rfl
id   └─┘
src  └─┘
typ  └─┘
251  
252  def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e
id                                       └─────────┘  
src                                            └─────────┘
typ                                      └─────────┘  
doc                                
253  
254  @[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) :
id                                                    
src                                  
typ                                                   
doc    └──┘                          
255    e.conj f x = (e $ f $ e.symm x) :=
id     └───┘           └───┘ 
src     └───┘                └───┘
typ    └───┘           └───┘ 
256  rfl
id   └─┘
src  └─┘
typ  └─┘
257  
258  @[simp] lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl
id                             └──┘  └────────┘    └────────┘          └─┘
src                            └──┘  └────────┘     └────────┘            └─┘
typ                            └──┘  └────────┘    └────────┘          └─┘
doc    └──┘
259  
260  @[simp] lemma conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl
id                                      └───┘└───┘  └───┘└───┘    └─┘
src                                        └───┘└───┘   └───┘└───┘    └─┘
typ                                     └───┘└───┘  └───┘└───┘    └─┘
doc    └──┘                         
261  
262  @[simp] lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
id                                              
src                                               
typ                                             
doc    └──┘                                       
263    (e₁.trans e₂).conj = e₁.conj.trans e₂.conj :=
id      └┘└────┘ └┘ └──┘   └┘└───┘└────┘ └┘└───┘
src       └────┘    └──┘     └───┘└────┘   └───┘
typ     └┘└────┘ └┘ └──┘   └┘└───┘└────┘ └┘└───┘
264  rfl
id   └─┘
src  └─┘
typ  └─┘
265  
266  @[simp] lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) :
id                                                
src                                 
typ                                               
doc    └──┘                         
267    e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) :=
id     └───┘  └┘  └┘    └───┘ └┘    └───┘ └┘
src     └───┘             └───┘        └───┘
typ    └───┘  └┘  └┘    └───┘ └┘    └───┘ └┘
268  by apply arrow_congr_comp
id            └──────────────┘
src     └────┘└──────────────┘
typ     └────┘└──────────────┘
doc     └────┘                
txt     └────┘                
par     └────┘                
pid                          
st     └───────────────────────
269  
src  
typ  
doc  
txt  
par  
pid  
st   
270  def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
id                           └───┘      └───┘
src                          └───┘      └───┘
typ                          └───┘      └───┘
doc                                    
271  ⟨λ _, punit.star, λ _, punit.star, λ u, by { cases u, refl }, λ u, by { cases u, reflexivity }⟩
id        └────────┘      └────────┘                                          
src        └────────┘       └────────┘            └────┘   └───┘             └────┘   └──────────┘
typ       └────────┘      └────────┘           └────┘  └───┘            └────┘  └──────────┘
doc                                               └────┘   └───┘             └────┘   └──────────┘
txt                                               └────┘   └───┘             └────┘   └──────────┘
par                                               └────┘   └───┘             └────┘   └──────────┘
pid                                                                                           
st                                             └────────┘└─────┘└┘        └────────┘└────────────┘└┘
272  
273  section
274  @[simp] def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
id                                                         └───┘       └───┘
src                                                         └───┘       └───┘
typ                                                        └───┘       └───┘
doc    └──┘                                                            
275  ⟨λ f, punit.star, λ u f, punit.star,
id        └────────┘       └────────┘
src        └────────┘         └────────┘
typ       └────────┘       └────────┘
276    λ f, by { funext x, cases f x, refl }, λ u, by { cases u, reflexivity }⟩
id                                                        
src              └──────┘  └────┘    └───┘             └────┘   └──────────┘
typ             └──────┘  └────┘  └───┘            └────┘  └──────────┘
doc              └──────┘  └────┘    └───┘             └────┘   └──────────┘
txt              └──────┘  └────┘    └───┘             └────┘   └──────────┘
par              └──────┘  └────┘    └───┘             └────┘   └──────────┘
pid                    └┘                                               
st            └─────────┘└─────────┘└─────┘└┘        └────────┘└────────────┘└┘
277  
278  @[simp] def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
id                                                └───┘          
src                                               └───┘          
typ                                               └───┘          
doc    └──┘                                                      
279  ⟨λ f, f punit.star, λ a u, a, λ f, by { funext x, cases x, refl }, λ u, rfl⟩
id         └────────┘                                                └─┘
src          └────────┘                      └──────┘  └────┘   └───┘        └─┘
typ        └────────┘                  └──────┘  └────┘  └───┘       └─┘
doc                                          └──────┘  └────┘   └───┘
txt                                          └──────┘  └────┘   └───┘
par                                          └──────┘  └────┘   └───┘
pid                                                └┘              
st                                        └─────────┘└───────┘└─────┘└┘
280  
281  @[simp] def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
id                                                      └───┘      └───┘
src                                                     └───┘       └───┘
typ                                                     └───┘      └───┘
doc    └──┘                                                        
282  ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
id        └────────┘       └──┘        └────┘       └──┘                   
src        └────────┘          └──┘         └────┘         └──┘              └────┘   └───┘
typ       └────────┘       └──┘        └────┘       └──┘             └────┘  └───┘
doc                                                                          └────┘   └───┘
txt                                                                          └────┘   └───┘
par                                                                          └────┘   └───┘
pid                                                                                      
st                                                                        └────────┘└─────┘└┘
283  
284  @[simp] def pempty_arrow_equiv_punit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
id                                                       └────┘      └───┘
src                                                      └────┘       └───┘
typ                                                      └────┘      └───┘
doc    └──┘                                              └────┘      
285  ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
id        └────────┘       └──┘        └────┘       └──┘                   
src        └────────┘          └──┘         └────┘         └──┘              └────┘   └───┘
typ       └────────┘       └──┘        └────┘       └──┘             └────┘  └───┘
doc                                                                          └────┘   └───┘
txt                                                                          └────┘   └───┘
par                                                                          └────┘   └───┘
pid                                                                                      
st                                                                        └────────┘└─────┘└┘
286  
287  @[simp] def false_arrow_equiv_punit (α : Sort*) : (false → α) ≃ punit.{u} :=
id                                                      └───┘      └───┘
src                                                     └───┘       └───┘
typ                                                     └───┘      └───┘
doc    └──┘                                                        
288  calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
id         └───┘        └───┘       └─────────┘ └───────────────┘  └────────┘
src        └───┘         └───┘        └─────────┘ └───────────────┘  └────────┘
typ        └───┘        └───┘       └─────────┘ └───────────────┘  └────────┘
289               ... ≃ punit       : empty_arrow_equiv_punit _
id                      └───┘         └─────────────────────┘
src                     └───┘         └─────────────────────┘
typ                     └───┘         └─────────────────────┘
290  
291  end
292  
293  @[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ :β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
id                                                       └┘  └┘       └┘  └┘    └┘  └┘  └┘  └┘
src    └───┘                                                                               
typ                                                      └┘  └┘       └┘  └┘    └┘  └┘  └┘  └┘
doc    └───┘                                                                            
294  ⟨λp, (e₁ p.1, e₂ p.2), λp, (e₁.symm p.1, e₂.symm p.2),
id       └┘    └┘        └┘└───┘    └┘└───┘ 
src                            └───┘       └───┘  
typ      └┘    └┘        └┘└───┘    └┘└───┘ 
295     λ ⟨a, b⟩, show (e₁.symm (e₁ a), e₂.symm (e₂ b)) = (a, b), by rw [symm_apply_apply, symm_apply_apply],
id                  └┘└───┘  └┘     └┘└───┘  └┘                    └──────────────┘  └──────────────┘
src                      └───┘           └───┘                    └──┘└──────────────┘└┘└──────────────┘
typ                 └┘└───┘  └┘     └┘└───┘  └┘                └──┘└──────────────┘└┘└──────────────┘
doc                                                                  └──┘                └┘                
txt                                                                  └──┘                └┘                
par                                                                  └──┘                └┘                
pid                                                                    └┘                └┘                
st                                                                  └───────────────────┘└────────────────┘
296     λ ⟨a, b⟩, show (e₁ (e₁.symm a), e₂ (e₂.symm b)) = (a, b), by rw [apply_symm_apply, apply_symm_apply]⟩
id                  └┘  └┘└───┘     └┘  └┘└───┘                    └──────────────┘  └──────────────┘
src                          └───┘           └───┘                └──┘└──────────────┘└┘└──────────────┘
typ                 └┘  └┘└───┘     └┘  └┘└───┘                └──┘└──────────────┘└┘└──────────────┘
doc                                                                  └──┘                └┘                
txt                                                                  └──┘                └┘                
par                                                                  └──┘                └┘                
pid                                                                    └┘                └┘                
st                                                                  └───────────────────┘└────────────────┘
297  
298  @[simp] theorem prod_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁) (b : β₁) :
id                                                                └┘  └┘        └┘  └┘       └┘       └┘
src                                                                                
typ                                                               └┘  └┘        └┘  └┘       └┘       └┘
doc    └──┘                                                                        
299    prod_congr e₁ e₂ (a, b) = (e₁ a, e₂ b) :=
id     └────────┘ └┘ └┘      └┘   └┘ 
src    └────────┘              
typ    └────────┘ └┘ └┘      └┘   └┘ 
300  rfl
id   └─┘
src  └─┘
typ  └─┘
301  
302  @[simp] def prod_comm (α β : Sort*) : α × β ≃ β × α :=
id                                               
src                                                
typ                                              
doc    └──┘                                      
303  ⟨λ p, (p.2, p.1), λ p, (p.2, p.1), λ⟨a, b⟩, rfl, λ⟨a, b⟩, rfl⟩
id                                  └─┘          └─┘
src                                        └─┘           └─┘
typ                                 └─┘          └─┘
304  
305  @[simp] def prod_assoc (α β γ : Sort*) : (α × β) × γ ≃ α × (β × γ) :=
id                                                         
src                                                            
typ                                                        
doc    └──┘                                               
306  ⟨λ p, ⟨p.1.1, ⟨p.1.2, p.2⟩⟩, λp, ⟨⟨p.1, p.2.1⟩, p.2.2⟩, λ ⟨⟨a, b⟩, c⟩, rfl, λ ⟨a, ⟨b, c⟩⟩, rfl⟩
id                                                       └─┘                └─┘
src                                                               └─┘                 └─┘
typ                                                      └─┘                └─┘
307  
308  @[simp] theorem prod_assoc_apply {α β γ : Sort*} (p : (α × β) × γ) :
id                                                               
src                                                               
typ                                                              
doc    └──┘
309    prod_assoc α β γ p = ⟨p.1.1, ⟨p.1.2, p.2⟩⟩ := rfl
id     └────────┘                       └─┘
src    └────────┘                              └─┘
typ    └────────┘                       └─┘
310  
311  section
312  @[simp] def prod_punit (α : Sort*) : α × punit.{u+1} ≃ α :=
id                                          └───┘        
src                                          └───┘       
typ                                         └───┘        
doc    └──┘                                               
313  ⟨λ p, p.1, λ a, (a, punit.star), λ ⟨_, punit.star⟩, rfl, λ a, rfl⟩
id                 └────────┘        └────────┘   └─┘      └─┘
src                    └────────┘         └────────┘   └─┘       └─┘
typ                └────────┘        └────────┘   └─┘      └─┘
314  
315  @[simp] theorem prod_punit_apply {α : Sort*} (a : α × punit.{u+1}) : prod_punit α a = a.1 := rfl
id                                                       └───┘          └────────┘         └─┘
src                                                       └───┘          └────────┘            └─┘
typ                                                      └───┘          └────────┘         └─┘
doc    └──┘
316  
317  @[simp] def punit_prod (α : Sort*) : punit.{u+1} × α ≃ α :=
id                                        └───┘          
src                                       └───┘          
typ                                       └───┘          
doc    └──┘                                               
318  calc punit × α ≃ α × punit : prod_comm _ _
id        └───┘       └───┘   └───────┘
src       └───┘         └───┘   └───────┘
typ       └───┘       └───┘   └───────┘
319             ... ≃ α         : prod_punit _
id                               └────────┘
src                               └────────┘
typ                              └────────┘
320  
321  @[simp] theorem punit_prod_apply {α : Sort*} (a : punit.{u+1} × α) : punit_prod α a = a.2 := rfl
id                                                     └───┘            └────────┘         └─┘
src                                                    └───┘             └────────┘            └─┘
typ                                                    └───┘            └────────┘         └─┘
doc    └──┘
322  
323  @[simp] def prod_empty (α : Sort*) : α × empty ≃ empty :=
id                                          └───┘  └───┘
src                                          └───┘  └───┘
typ                                         └───┘  └───┘
doc    └──┘                                         
324  equiv_empty (λ ⟨_, e⟩, e.rec _)
id   └─────────┘           └──┘
src  └─────────┘             └──┘
typ  └─────────┘           └──┘
325  
326  @[simp] def empty_prod (α : Sort*) : empty × α ≃ empty :=
id                                        └───┘    └───┘
src                                       └───┘     └───┘
typ                                       └───┘    └───┘
doc    └──┘                                         
327  equiv_empty (λ ⟨e, _⟩, e.rec _)
id   └─────────┘           └──┘
src  └─────────┘             └──┘
typ  └─────────┘           └──┘
328  
329  @[simp] def prod_pempty (α : Sort*) : α × pempty ≃ pempty :=
id                                           └────┘  └────┘
src                                           └────┘  └────┘
typ                                          └────┘  └────┘
doc    └──┘                                    └────┘  └────┘
330  equiv_pempty (λ ⟨_, e⟩, e.rec _)
id   └──────────┘           └──┘
src  └──────────┘             └──┘
typ  └──────────┘           └──┘
331  
332  @[simp] def pempty_prod (α : Sort*) : pempty × α ≃ pempty :=
id                                         └────┘    └────┘
src                                        └────┘     └────┘
typ                                        └────┘    └────┘
doc    └──┘                                └────┘      └────┘
333  equiv_pempty (λ ⟨e, _⟩, e.rec _)
id   └──────────┘           └──┘
src  └──────────┘             └──┘
typ  └──────────┘           └──┘
334  end
335  
336  section
337  open sum
338  def psum_equiv_sum (α β : Sort*) : psum α β ≃ α ⊕ β :=
id                                      └──┘      
src                                     └──┘        
typ                                     └──┘      
doc                                              
339  ⟨λ s, psum.cases_on s inl inr,
id        └───────────┘  └─┘ └─┘
src        └───────────┘   └─┘ └─┘
typ       └───────────┘  └─┘ └─┘
340   λ s, sum.cases_on s psum.inl psum.inr,
id        └──────────┘  └──────┘ └──────┘
src        └──────────┘   └──────┘ └──────┘
typ       └──────────┘  └──────┘ └──────┘
341   λ s, by cases s; refl,
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
342   λ s, by cases s; refl⟩
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
343  
344  def sum_congr {α₁ β₁ α₂ β₂ : Sort*} : α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
id                                         └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘
src                                                                     
typ                                        └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘
doc                                                                  
345  | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ :=
id      └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘
typ     └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘
346    ⟨λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end,
id                      └─┘ └┘    └─┘           └─┘ └┘    └─┘
src                       └─┘       └─┘           └─┘       └─┘
typ                     └─┘ └┘    └─┘           └─┘ └┘    └─┘
347     λ s, match s with inl a₂ := inl (g₁ a₂) | inr b₂ := inr (g₂ b₂) end,
id                      └─┘ └┘    └─┘           └─┘ └┘    └─┘
src                       └─┘       └─┘           └─┘       └─┘
typ                     └─┘ └┘    └─┘           └─┘ └┘    └─┘
348     λ s, match s with inl a := congr_arg inl (l₁ a) | inr a := congr_arg inr (l₂ a) end,
id                      └─┘     └───────┘ └─┘          └─┘     └───────┘ └─┘
src                       └─┘      └───────┘ └─┘          └─┘      └───────┘ └─┘
typ                     └─┘     └───────┘ └─┘          └─┘     └───────┘ └─┘
349     λ s, match s with inl a := congr_arg inl (r₁ a) | inr a := congr_arg inr (r₂ a) end⟩
id                      └─┘     └───────┘ └─┘          └─┘     └───────┘ └─┘
src                       └─┘      └───────┘ └─┘          └─┘      └───────┘ └─┘
typ                     └─┘     └───────┘ └─┘          └─┘     └───────┘ └─┘
350  
351  @[simp] theorem sum_congr_apply_inl {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁) :
id                                                                   └┘  └┘        └┘  └┘       └┘
src                                                                                   
typ                                                                  └┘  └┘        └┘  └┘       └┘
doc    └──┘                                                                           
352    sum_congr e₁ e₂ (inl a) = inl (e₁ a) :=
id     └───────┘ └┘ └┘  └─┘    └─┘  └┘ 
src    └───────┘        └─┘     └─┘
typ    └───────┘ └┘ └┘  └─┘    └─┘  └┘ 
353  by { cases e₁, cases e₂, refl }
id              └┘        └┘
src       └────┘    └────┘    └───┘
typ       └────┘└┘  └────┘└┘  └───┘
doc       └────┘    └────┘    └───┘
txt       └────┘    └────┘    └───┘
par       └────┘    └────┘    └───┘
pid                             
st     └─────────┘└────────┘└─────┘└┘
354  
355  @[simp] theorem sum_congr_apply_inr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (b : β₁) :
id                                                                   └┘  └┘        └┘  └┘       └┘
src                                                                                   
typ                                                                  └┘  └┘        └┘  └┘       └┘
doc    └──┘                                                                           
356    sum_congr e₁ e₂ (inr b) = inr (e₂ b) :=
id     └───────┘ └┘ └┘  └─┘    └─┘  └┘ 
src    └───────┘        └─┘     └─┘
typ    └───────┘ └┘ └┘  └─┘    └─┘  └┘ 
357  by { cases e₁, cases e₂, refl }
id              └┘        └┘
src       └────┘    └────┘    └───┘
typ       └────┘└┘  └────┘└┘  └───┘
doc       └────┘    └────┘    └───┘
txt       └────┘    └────┘    └───┘
par       └────┘    └────┘    └───┘
pid                             
st     └─────────┘└────────┘└─────┘└┘
358  
359  @[simp] lemma sum_congr_symm {α β γ δ : Type u} (e : α ≃ β) (f : γ ≃ δ) (x) :
id                                                                   
src                                                                    
typ                                                                  
doc    └──┘                                                            
360    (equiv.sum_congr e f).symm x = (equiv.sum_congr (e.symm) (f.symm)) x :=
id      └─────────────┘   └──┘     └─────────────┘  └───┘   └───┘   
src     └─────────────┘     └──┘      └─────────────┘   └───┘    └───┘
typ     └─────────────┘   └──┘     └─────────────┘  └───┘   └───┘   
361  by { cases e, cases f, cases x; refl }
id                              
src       └────┘   └────┘   └────┘   └───┘
typ       └────┘  └────┘  └────┘  └───┘
doc       └────┘   └────┘   └────┘   └───┘
txt       └────┘   └────┘   └────┘   └───┘
par       └────┘   └────┘   └────┘   └───┘
pid                                   
st     └────────┘└───────┘└──────────────┘└┘
362  
363  def bool_equiv_punit_sum_punit : bool ≃ punit.{u+1} ⊕ punit.{v+1} :=
id                                    └──┘  └───┘        └───┘
src                                   └──┘  └───┘        └───┘
typ                                   └──┘  └───┘        └───┘
doc                                        
364  ⟨λ b, cond b (inr punit.star) (inl punit.star),
id        └──┘   └─┘ └────────┘   └─┘ └────────┘
src        └──┘    └─┘ └────────┘   └─┘ └────────┘
typ       └──┘   └─┘ └────────┘   └─┘ └────────┘
365   λ s, sum.rec_on s (λ_, ff) (λ_, tt),
id        └────────┘      └┘      └┘
src        └────────┘        └┘       └┘
typ       └────────┘      └┘      └┘
366   λ b, by cases b; refl,
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
367   λ s, by rcases s with ⟨⟨⟩⟩ | ⟨⟨⟩⟩; refl⟩
id                  
src           └─────┘ └───────────────┘  └──┘
typ          └─────┘└───────────────┘  └──┘
doc           └─────┘ └───────────────┘  └──┘
txt           └─────┘ └───────────────┘  └──┘
par           └─────┘ └───────────────┘  └──┘
pid                  └───────────────┘
st           └──────────────────────────────┘
368  
369  noncomputable def Prop_equiv_bool : Prop ≃ bool :=
id                                             └──┘
src                                            └──┘
typ                                            └──┘
doc                                           
370  ⟨λ p, @to_bool p (classical.prop_decidable _),
id         └─────┘   └──────────────────────┘
src         └─────┘    └──────────────────────┘
typ        └─────┘   └──────────────────────┘
371   λ b, b, λ p, by simp, λ b, by simp⟩
id                         
src                   └──┘          └──┘
typ                └──┘         └──┘
doc                   └──┘          └──┘
txt                   └──┘          └──┘
par                   └──┘          └──┘
st                   └───┘         └───┘
372  
373  @[simp] def sum_comm (α β : Sort*) : α ⊕ β ≃ β ⊕ α :=
id                                              
src                                               
typ                                             
doc    └──┘                                     
374  ⟨λ s, match s with inl a := inr a | inr b := inl b end,
id                    └─┘     └─┘     └─┘     └─┘
src                     └─┘      └─┘     └─┘      └─┘
typ                   └─┘     └─┘     └─┘     └─┘
375   λ s, match s with inl b := inr b | inr a := inl a end,
id                    └─┘     └─┘     └─┘     └─┘
src                     └─┘      └─┘     └─┘      └─┘
typ                   └─┘     └─┘     └─┘     └─┘
376   λ s, by cases s; refl,
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
377   λ s, by cases s; refl⟩
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
378  
379  @[simp] def sum_assoc (α β γ : Sort*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
id                                                        
src                                                           
typ                                                       
doc    └──┘                                              
380  ⟨λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end,
id                         └─┘      └─┘     └─┘  └─┘      └─┘  └─┘      └─┘     └─┘  └─┘
src                          └─┘       └─┘     └─┘  └─┘       └─┘  └─┘      └─┘      └─┘  └─┘
typ                        └─┘      └─┘     └─┘  └─┘      └─┘  └─┘      └─┘     └─┘  └─┘
381   λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end,
id                    └─┘     └─┘  └─┘      └─┘  └─┘      └─┘  └─┘           └─┘      └─┘
src                     └─┘      └─┘  └─┘      └─┘  └─┘       └─┘  └─┘           └─┘       └─┘
typ                   └─┘     └─┘  └─┘      └─┘  └─┘      └─┘  └─┘           └─┘      └─┘
382   λ s, by rcases s with ⟨_ | _⟩ | _; refl,
id                  
src           └─────┘ └───────────────┘  └──┘
typ          └─────┘└───────────────┘  └──┘
doc           └─────┘ └───────────────┘  └──┘
txt           └─────┘ └───────────────┘  └──┘
par           └─────┘ └───────────────┘  └──┘
pid                  └───────────────┘
st           └──────────────────────────────┘
383   λ s, by rcases s with _ | _ | _; refl⟩
id                  
src           └─────┘ └─────────────┘  └──┘
typ          └─────┘└─────────────┘  └──┘
doc           └─────┘ └─────────────┘  └──┘
txt           └─────┘ └─────────────┘  └──┘
par           └─────┘ └─────────────┘  └──┘
pid                  └─────────────┘
st           └────────────────────────────┘
384  
385  @[simp] theorem sum_assoc_apply_in1 {α β γ} (a) : sum_assoc α β γ (inl (inl a)) = inl a := rfl
id                                                     └───────┘     └─┘  └─┘     └─┘     └─┘
src                                                    └───────┘        └─┘  └─┘      └─┘      └─┘
typ                                                    └───────┘     └─┘  └─┘     └─┘     └─┘
doc    └──┘
386  @[simp] theorem sum_assoc_apply_in2 {α β γ} (b) : sum_assoc α β γ (inl (inr b)) = inr (inl b) := rfl
id                                                     └───────┘     └─┘  └─┘     └─┘  └─┘      └─┘
src                                                    └───────┘        └─┘  └─┘      └─┘  └─┘       └─┘
typ                                                    └───────┘     └─┘  └─┘     └─┘  └─┘      └─┘
doc    └──┘
387  @[simp] theorem sum_assoc_apply_in3 {α β γ} (c) : sum_assoc α β γ (inr c) = inr (inr c) := rfl
id                                                     └───────┘     └─┘    └─┘  └─┘      └─┘
src                                                    └───────┘        └─┘     └─┘  └─┘       └─┘
typ                                                    └───────┘     └─┘    └─┘  └─┘      └─┘
doc    └──┘
388  
389  @[simp] def sum_empty (α : Sort*) : α ⊕ empty ≃ α :=
id                                         └───┘  
src                                         └───┘ 
typ                                        └───┘  
doc    └──┘                                        
390  ⟨λ s, match s with inl a := a | inr e := empty.rec _ e end,
id                    └─┘         └─┘     └───────┘
src                     └─┘          └─┘      └───────┘
typ                   └─┘         └─┘     └───────┘
391   inl,
id    └─┘
src   └─┘
typ   └─┘
392   λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
id                    
src             └─────┘ └────────────┘  └───┘
typ            └─────┘└────────────┘  └───┘
doc             └─────┘ └────────────┘  └───┘
txt             └─────┘ └────────────┘  └───┘
par             └─────┘ └────────────┘  └───┘
pid                    └────────────┘      
st           └───────────────────────┘└─────┘└┘
393   λ a, rfl⟩
id        └─┘
src        └─┘
typ       └─┘
394  
395  @[simp] def empty_sum (α : Sort*) : empty ⊕ α ≃ α :=
id                                       └───┘    
src                                      └───┘    
typ                                      └───┘    
doc    └──┘                                        
396  (sum_comm _ _).trans $ sum_empty _
id    └──────┘     └───┘    └───────┘
src   └──────┘     └───┘    └───────┘
typ   └──────┘     └───┘    └───────┘
397  
398  @[simp] def sum_pempty (α : Sort*) : α ⊕ pempty ≃ α :=
id                                          └────┘  
src                                          └────┘ 
typ                                         └────┘  
doc    └──┘                                   └────┘ 
399  ⟨λ s, match s with inl a := a | inr e := pempty.rec _ e end,
id                    └─┘         └─┘     └────────┘
src                     └─┘          └─┘      └────────┘
typ                   └─┘         └─┘     └────────┘
400   inl,
id    └─┘
src   └─┘
typ   └─┘
401   λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
id                    
src             └─────┘ └────────────┘  └───┘
typ            └─────┘└────────────┘  └───┘
doc             └─────┘ └────────────┘  └───┘
txt             └─────┘ └────────────┘  └───┘
par             └─────┘ └────────────┘  └───┘
pid                    └────────────┘      
st           └───────────────────────┘└─────┘└┘
402   λ a, rfl⟩
id        └─┘
src        └─┘
typ       └─┘
403  
404  @[simp] def pempty_sum (α : Sort*) : pempty ⊕ α ≃ α :=
id                                        └────┘    
src                                       └────┘    
typ                                       └────┘    
doc    └──┘                               └────┘     
405  (sum_comm _ _).trans $ sum_pempty _
id    └──────┘     └───┘    └────────┘
src   └──────┘     └───┘    └────────┘
typ   └──────┘     └───┘    └────────┘
406  
407  @[simp] def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
id                                                    └────┘     └───┘
src                                                   └────┘       └───┘
typ                                                   └────┘     └───┘
doc    └──┘                                                    
408  ⟨λ o, match o with none := inr punit.star | some a := inl a end,
id                    └──┘    └─┘ └────────┘   └──┘     └─┘
src                     └──┘    └─┘ └────────┘   └──┘      └─┘
typ                   └──┘    └─┘ └────────┘   └──┘     └─┘
409   λ s, match s with inr _ := none | inl a := some a end,
id                    └─┘      └──┘   └─┘     └──┘
src                     └─┘      └──┘   └─┘      └──┘
typ                   └─┘      └──┘   └─┘     └──┘
410   λ o, by cases o; refl,
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
411   λ s, by rcases s with _ | ⟨⟨⟩⟩; refl⟩
id                  
src           └─────┘ └────────────┘  └──┘
typ          └─────┘└────────────┘  └──┘
doc           └─────┘ └────────────┘  └──┘
txt           └─────┘ └────────────┘  └──┘
par           └─────┘ └────────────┘  └──┘
pid                  └────────────┘
st           └───────────────────────────┘
412  
413  def sum_equiv_sigma_bool (α β : Sort*) : α ⊕ β ≃ (Σ b: bool, cond b α β) :=
id                                                     └──┘ └──┘   
src                                                      └──┘ └──┘
typ                                                    └──┘ └──┘   
doc                                                 
414  ⟨λ s, match s with inl a := ⟨tt, a⟩ | inr b := ⟨ff, b⟩ end,
id                    └─┘      └┘       └─┘      └┘
src                     └─┘       └┘       └─┘       └┘
typ                   └─┘      └┘       └─┘      └┘
415   λ s, match s with ⟨tt, a⟩ := inl a | ⟨ff, b⟩ := inr b end,
id                     └┘       └─┘      └┘       └─┘
src                      └┘        └─┘      └┘        └─┘
typ                    └┘       └─┘      └┘       └─┘
416   λ s, by cases s; refl,
id                 
src           └────┘   └──┘
typ          └────┘  └──┘
doc           └────┘   └──┘
txt           └────┘   └──┘
par           └────┘   └──┘
pid                
st           └────────────┘
417   λ s, by rcases s with ⟨_|_, _⟩; refl⟩
id                  
src           └─────┘ └────────────┘  └──┘
typ          └─────┘└────────────┘  └──┘
doc           └─────┘ └────────────┘  └──┘
txt           └─────┘ └────────────┘  └──┘
par           └─────┘ └────────────┘  └──┘
pid                  └────────────┘
st           └───────────────────────────┘
418  
419  def sigma_preimage_equiv {α β : Type*} (f : α → β) :
id                                                  
typ                                                 
420    (Σ y : β, {x // f x = y}) ≃ α :=
id                       
src                          
typ                      
doc                              
421  ⟨λ x, x.2.1, λ x, ⟨f x, x, rfl⟩, λ ⟨y, x, rfl⟩, rfl, λ x, rfl⟩
id                      └─┘           └─┘   └─┘      └─┘
src                           └─┘            └─┘   └─┘       └─┘
typ                     └─┘           └─┘   └─┘      └─┘
422  
423  end
424  
425  section
426  
427  def Pi_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (Π a, β₁ a) ≃ (Π a, β₂ a) :=
id                                                      └┘   └┘          └┘         └┘ 
src                                                                                 
typ                                                     └┘   └┘          └┘         └┘ 
doc                                                                                 
428  ⟨λ H a, F a (H a), λ H a, (F a).symm (H a),
id                        └──┘    
src                                 └──┘
typ                       └──┘    
429   λ H, funext $ by simp, λ H, funext $ by simp⟩
id        └────┘                └────┘
src        └────┘      └──┘       └────┘      └──┘
typ       └────┘      └──┘      └────┘      └──┘
doc                    └──┘                   └──┘
txt                    └──┘                   └──┘
par                    └──┘                   └──┘
st                    └───┘                  └───┘
430  
431  def Pi_curry {α} {β : α → Sort*} (γ : Π a, β a → Sort*) : (Π x : sigma β, γ x.1 x.2) ≃ (Π a b, γ a b) :=
id                                                                └───┘                  
src                                                                   └───┘             
typ                                                               └───┘                  
doc                                                                                       
432  { to_fun := λ f x y, f ⟨x,y⟩,
id                        
typ                       
433    inv_fun := λ f x, f x.1 x.2,
id                        
src                            
typ                       
434    left_inv := λ f, funext $ λ ⟨x,y⟩, rfl,
id                     └────┘           └─┘
src                     └────┘            └─┘
typ                    └────┘           └─┘
435    right_inv := λ f, funext $ λ x, funext $ λ y, rfl }
id                      └────┘       └────┘       └─┘
src                      └────┘        └────┘        └─┘
typ                     └────┘       └────┘       └─┘
436  
437  end
438  
439  section
440  def psigma_equiv_sigma {α} (β : α → Sort*) : psigma β ≃ sigma β :=
id                                               └────┘   └───┘ 
src                                               └────┘    └───┘
typ                                              └────┘   └───┘ 
doc                                                        
441  ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
id                                           └─┘           └─┘
src                                                 └─┘            └─┘
typ                                          └─┘           └─┘
442  
443  def sigma_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : sigma β₁ ≃ sigma β₂ :=
id                                                         └┘   └┘     └───┘ └┘  └───┘ └┘
src                                                                        └───┘     └───┘
typ                                                        └┘   └┘     └───┘ └┘  └───┘ └┘
doc                                                                                 
444  ⟨λ ⟨a, b⟩, ⟨a, F a b⟩, λ ⟨a, b⟩, ⟨a, (F a).symm b⟩,
id                                     └──┘
src                                            └──┘
typ                                    └──┘
445   λ ⟨a, b⟩, congr_arg (sigma.mk a) $ symm_apply_apply (F a) b,
id           └───────┘  └──────┘      └──────────────┘  
src             └───────┘  └──────┘      └──────────────┘
typ          └───────┘  └──────┘      └──────────────┘  
446   λ ⟨a, b⟩, congr_arg (sigma.mk a) $ apply_symm_apply (F a) b⟩
id           └───────┘  └──────┘      └──────────────┘  
src             └───────┘  └──────┘      └──────────────┘
typ          └───────┘  └──────┘      └──────────────┘  
447  
448  def sigma_congr_left {α₁ α₂} {β : α₂ → Sort*} : ∀ f : α₁ ≃ α₂, (Σ a:α₁, β (f a)) ≃ (Σ a:α₂, β a)
id                                     └┘                 └┘  └┘      └┘            └┘  
src                                                                                       
typ                                    └┘                 └┘  └┘      └┘            └┘  
doc                                                                                  
449  | ⟨f, g, l, r⟩ :=
id            
typ           
450    ⟨λ ⟨a, b⟩, ⟨f a, b⟩, λ ⟨a, b⟩, ⟨g a, @@eq.rec β b (r a).symm⟩,
id                                      └────┘         └──┘
src                                           └────┘          └──┘
typ                                     └────┘         └──┘
451     λ ⟨a, b⟩, match g (f a), l a : ∀ a' (h : a' = a),
id                                            └┘ 
src                                                 
typ                                           └┘ 
452         @sigma.mk _ (β ∘ f) _ (@@eq.rec β b (congr_arg f h.symm)) = ⟨a, b⟩ with
id           └──────┘              └────┘     └───────┘   └───┘   
src          └──────┘               └────┘      └───────┘    └───┘   
typ          └──────┘              └────┘     └───────┘   └───┘   
453       | _, rfl := rfl end,
id             └─┘    └─┘
src            └─┘    └─┘
typ            └─┘    └─┘
454     λ ⟨a, b⟩, match f (g a), _ : ∀ a' (h : a' = a), sigma.mk a' (@@eq.rec β b h.symm) = ⟨a, b⟩ with
id                                          └┘      └──────┘ └┘    └────┘    └───┘  
src                                                    └──────┘       └────┘      └───┘  
typ                                         └┘      └──────┘ └┘    └────┘    └───┘  
455       | _, rfl := rfl end⟩
id             └─┘    └─┘
src            └─┘    └─┘
typ            └─┘    └─┘
456  
457  def sigma_equiv_prod (α β : Sort*) : (Σ_:α, β) ≃ α × β :=
id                                                 
src                                                  
typ                                                
doc                                                 
458  ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
id                                           └─┘           └─┘
src                                                 └─┘            └─┘
typ                                          └─┘           └─┘
459  
460  def sigma_equiv_prod_of_equiv {α β} {β₁ : α → Sort*} (F : ∀ a, β₁ a ≃ β) : sigma β₁ ≃ α × β :=
id                                                                └┘       └───┘ └┘    
src                                                                            └───┘       
typ                                                               └┘       └───┘ └┘    
doc                                                                                     
461  (sigma_congr_right F).trans (sigma_equiv_prod α β)
id    └───────────────┘  └───┘   └──────────────┘  
src   └───────────────┘   └───┘   └──────────────┘
typ   └───────────────┘  └───┘   └──────────────┘  
462  
463  end
464  
465  section
466  def arrow_prod_equiv_prod_arrow (α β γ : Type*) : (γ → α × β) ≃ (γ → α) × (γ → β) :=
id                                                                         
src                                                                        
typ                                                                        
doc                                                                
467  ⟨λ f, (λ c, (f c).1, λ c, (f c).2),
id                         
src                               
typ                        
468   λ p c, (p.1 c, p.2 c),
id               
src                 
typ              
469   λ f, funext $ λ c, prod.mk.eta,
id        └────┘       └─────────┘
src        └────┘        └─────────┘
typ       └────┘       └─────────┘
470   λ p, by { cases p, refl }⟩
id                   
src             └────┘   └───┘
typ            └────┘  └───┘
doc             └────┘   └───┘
txt             └────┘   └───┘
par             └────┘   └───┘
pid                         
st           └────────┘└─────┘└┘
471  
472  def arrow_arrow_equiv_prod_arrow (α β γ : Sort*) : (α → β → γ) ≃ (α × β → γ) :=
id                                                                      
src                                                                     
typ                                                                     
doc                                                                 
473  ⟨λ f, λ p, f p.1 p.2,
id               
src                   
typ              
474   λ f, λ a b, f (a, b),
id                
src                 
typ               
475   λ f, rfl,
id        └─┘
src        └─┘
typ       └─┘
476   λ f, by { funext p, cases p, refl }⟩
id                             
src             └──────┘  └────┘   └───┘
typ            └──────┘  └────┘  └───┘
doc             └──────┘  └────┘   └───┘
txt             └──────┘  └────┘   └───┘
par             └──────┘  └────┘   └───┘
pid                   └┘              
st           └─────────┘└───────┘└─────┘└┘
477  
478  open sum
479  def sum_arrow_equiv_prod_arrow (α β γ : Type*) : ((α ⊕ β) → γ) ≃ (α → γ) × (β → γ) :=
id                                                                          
src                                                                         
typ                                                                         
doc                                                                 
480  ⟨λ f, (f ∘ inl, f ∘ inr),
id          └─┘    └─┘
src           └─┘     └─┘
typ         └─┘    └─┘
481   λ p s, sum.rec_on s p.1 p.2,
id         └────────┘    
src          └────────┘       
typ        └────────┘    
482   λ f, by { funext s, cases s; refl },
id                             
src             └──────┘  └────┘   └───┘
typ            └──────┘  └────┘  └───┘
doc             └──────┘  └────┘   └───┘
txt             └──────┘  └────┘   └───┘
par             └──────┘  └────┘   └───┘
pid                   └┘              
st           └─────────┘└──────────────┘└┘
483   λ p, by { cases p, refl }⟩
id                   
src             └────┘   └───┘
typ            └────┘  └───┘
doc             └────┘   └───┘
txt             └────┘   └───┘
par             └────┘   └───┘
pid                         
st           └────────┘└─────┘└┘
484  
485  def sum_prod_distrib (α β γ : Sort*) : (α ⊕ β) × γ ≃ (α × γ) ⊕ (β × γ) :=
id                                                           
src                                                               
typ                                                          
doc                                                     
486  ⟨λ p, match p with (inl a, c) := inl (a, c) | (inr b, c) := inr (b, c) end,
id                    └─┘        └─┘         └─┘        └─┘ 
src                     └─┘          └─┘         └─┘          └─┘ 
typ                   └─┘        └─┘         └─┘        └─┘ 
487   λ s, match s with inl (a, c) := (inl a, c) | inr (b, c) := (inr b, c) end,
id                    └─┘        └─┘         └─┘        └─┘
src                     └─┘          └─┘         └─┘          └─┘
typ                   └─┘        └─┘         └─┘        └─┘
488   λ p, by rcases p with ⟨_ | _, _⟩; refl,
id                  
src           └─────┘ └──────────────┘  └──┘
typ          └─────┘└──────────────┘  └──┘
doc           └─────┘ └──────────────┘  └──┘
txt           └─────┘ └──────────────┘  └──┘
par           └─────┘ └──────────────┘  └──┘
pid                  └──────────────┘
st           └─────────────────────────────┘
489   λ s, by rcases s with ⟨_, _⟩ | ⟨_, _⟩; refl⟩
id                  
src           └─────┘ └───────────────────┘  └──┘
typ          └─────┘└───────────────────┘  └──┘
doc           └─────┘ └───────────────────┘  └──┘
txt           └─────┘ └───────────────────┘  └──┘
par           └─────┘ └───────────────────┘  └──┘
pid                  └───────────────────┘
st           └──────────────────────────────────┘
490  
491  @[simp] theorem sum_prod_distrib_apply_left {α β γ} (a : α) (c : γ) :
id                                                                   
typ                                                                  
doc    └──┘
492     sum_prod_distrib α β γ (sum.inl a, c) = sum.inl (a, c) := rfl
id      └──────────────┘    └─────┘      └─────┘        └─┘
src     └──────────────┘       └─────┘        └─────┘          └─┘
typ     └──────────────┘    └─────┘      └─────┘        └─┘
493  @[simp] theorem sum_prod_distrib_apply_right {α β γ} (b : β) (c : γ) :
id                                                                    
typ                                                                   
doc    └──┘
494     sum_prod_distrib α β γ (sum.inr b, c) = sum.inr (b, c) := rfl
id      └──────────────┘    └─────┘      └─────┘        └─┘
src     └──────────────┘       └─────┘        └─────┘          └─┘
typ     └──────────────┘    └─────┘      └─────┘        └─┘
495  
496  def prod_sum_distrib (α β γ : Sort*) : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ) :=
id                                                           
src                                                               
typ                                                          
doc                                                     
497  calc α × (β ⊕ γ) ≃ (β ⊕ γ) × α       : prod_comm _ _
id                                └───────┘
src                                     └───────┘
typ                               └───────┘
498              ...   ≃ (β × α) ⊕ (γ × α) : sum_prod_distrib _ _ _
id                                    └──────────────┘
src                                       └──────────────┘
typ                                   └──────────────┘
499              ...   ≃ (α × β) ⊕ (α × γ) : sum_congr (prod_comm _ _) (prod_comm _ _)
id                                    └───────┘  └───────┘       └───────┘
src                                       └───────┘  └───────┘       └───────┘
typ                                   └───────┘  └───────┘       └───────┘
500  
501  @[simp] theorem prod_sum_distrib_apply_left {α β γ} (a : α) (b : β) :
id                                                                   
typ                                                                  
doc    └──┘
502     prod_sum_distrib α β γ (a, sum.inl b) = sum.inl (a, b) := rfl
id      └──────────────┘      └─────┘    └─────┘        └─┘
src     └──────────────┘          └─────┘     └─────┘          └─┘
typ     └──────────────┘      └─────┘    └─────┘        └─┘
503  @[simp] theorem prod_sum_distrib_apply_right {α β γ} (a : α) (c : γ) :
id                                                                    
typ                                                                   
doc    └──┘
504     prod_sum_distrib α β γ (a, sum.inr c) = sum.inr (a, c) := rfl
id      └──────────────┘      └─────┘    └─────┘        └─┘
src     └──────────────┘          └─────┘     └─────┘          └─┘
typ     └──────────────┘      └─────┘    └─────┘        └─┘
505  
506  def sigma_prod_distrib {ι : Type*} (α : ι → Type*) (β : Type*) :
id                                           
typ                                          
507    ((Σ i, α i) × β) ≃ (Σ i, (α i × β)) :=
id                       
src                            
typ                      
doc                     
508  ⟨λ p, ⟨p.1.1, (p.1.2, p.2)⟩,
id                 
src                    
typ                
509   λ p, (⟨p.1, p.2.1⟩, p.2.2),
id                  
src                     
typ                 
510   λ p, by { rcases p with ⟨⟨_, _⟩, _⟩, refl },
id                    
src             └─────┘ └───────────────┘  └───┘
typ            └─────┘└───────────────┘  └───┘
doc             └─────┘ └───────────────┘  └───┘
txt             └─────┘ └───────────────┘  └───┘
par             └─────┘ └───────────────┘  └───┘
pid                    └───────────────┘      
st           └──────────────────────────┘└─────┘└┘
511   λ p, by { rcases p with ⟨_, ⟨_, _⟩⟩, refl }⟩
id                    
src             └─────┘ └───────────────┘  └───┘
typ            └─────┘└───────────────┘  └───┘
doc             └─────┘ └───────────────┘  └───┘
txt             └─────┘ └───────────────┘  └───┘
par             └─────┘ └───────────────┘  └───┘
pid                    └───────────────┘      
st           └──────────────────────────┘└─────┘└┘
512  
513  def bool_prod_equiv_sum (α : Type u) : bool × α ≃ α ⊕ α :=
id                                          └──┘      
src                                         └──┘       
typ                                         └──┘      
doc                                                  
514  calc bool × α ≃ (unit ⊕ unit) × α       : prod_congr bool_equiv_punit_sum_punit (equiv.refl _)
id        └──┘      └──┘  └──┘            └────────┘ └────────────────────────┘  └────────┘
src       └──┘       └──┘  └──┘             └────────┘ └────────────────────────┘  └────────┘
typ       └──┘      └──┘  └──┘            └────────┘ └────────────────────────┘  └────────┘
doc                   └──┘   └──┘
515        ...     ≃ α × (unit ⊕ unit)       : prod_comm _ _
id                      └──┘  └──┘          └───────┘
src                      └──┘  └──┘          └───────┘
typ                     └──┘  └──┘          └───────┘
doc                       └──┘   └──┘
516        ...     ≃ (α × unit) ⊕ (α × unit) : prod_sum_distrib _ _ _
id                      └──┘      └──┘    └──────────────┘
src                      └──┘       └──┘    └──────────────┘
typ                     └──┘      └──┘    └──────────────┘
doc                       └──┘         └──┘
517        ...     ≃ α ⊕ α                   : sum_congr (prod_punit _) (prod_punit _)
id                                          └───────┘  └────────┘     └────────┘
src                                           └───────┘  └────────┘     └────────┘
typ                                         └───────┘  └────────┘     └────────┘
518  end
519  
520  section
521  open sum nat
522  def nat_equiv_nat_sum_punit : ℕ ≃ ℕ ⊕ punit.{u+1} :=
id                                     └───┘
src                                    └───┘
typ                                    └───┘
doc                                  
523  ⟨λ n, match n with zero := inr punit.star | succ a := inl a end,
id                    └──┘    └─┘ └────────┘   └──┘     └─┘
src                     └──┘    └─┘ └────────┘   └──┘      └─┘
typ                   └──┘    └─┘ └────────┘   └──┘     └─┘
524   λ s, match s with inl n := succ n | inr punit.star := zero end,
id                    └─┘     └──┘     └─┘ └────────┘    └──┘
src                     └─┘      └──┘     └─┘ └────────┘    └──┘
typ                   └─┘     └──┘     └─┘ └────────┘    └──┘
525   λ n, begin cases n, repeat { refl } end,
id                    
src              └────┘   └───────┘└───┘└┘
typ             └────┘  └───────┘└───┘└┘
doc              └────┘   └───────┘└───┘└┘
txt              └────┘   └───────┘└───┘└┘
par              └────┘   └───────┘└───┘└┘
pid                            └───────┘
st         └───────────┘└────────┘└────┘└─┘
526   λ s, begin cases s with a u, { refl }, {cases u, { refl }} end⟩
id                                                
src              └────┘ └───────┘    └───┘    └────┘     └───┘
typ             └────┘└───────┘    └───┘    └────┘    └───┘
doc              └────┘ └───────┘    └───┘    └────┘     └───┘
txt              └────┘ └───────┘    └───┘    └────┘     └───┘
par              └────┘ └───────┘    └───┘    └────┘     └───┘
pid                    └───────┘                          
st         └────────────────────┘└──┘└───┘└┘└───────┘└───────┘└────┘
527  
528  @[simp] def nat_sum_punit_equiv_nat : ℕ ⊕ punit.{u+1} ≃ ℕ :=
id                                           └───┘        
src                                          └───┘        
typ                                          └───┘        
doc    └──┘                                                
529  nat_equiv_nat_sum_punit.symm
id   └─────────────────────┘└───┘
src  └─────────────────────┘└───┘
typ  └─────────────────────┘└───┘
530  
531  def int_equiv_nat_sum_nat : ℤ ≃ ℕ ⊕ ℕ :=
id                                   
src                                  
typ                                  
doc                                
532  by refine ⟨_, _, _, _⟩; intro z; {cases z; [left, right]; assumption} <|> {cases z; refl}
id                                                                                  
src     └─────┘ └─────────┘  └─────┘   └────┘   └──┘  └───┘   └────────┘       └────┘   └──┘
typ     └─────┘ └─────────┘  └─────┘   └────┘  └──┘  └───┘   └────────┘       └────┘  └──┘
doc     └─────┘ └─────────┘  └─────┘   └────┘    └──┘  └───┘   └────────┘       └────┘   └──┘
txt     └─────┘ └─────────┘  └─────┘   └────┘    └──┘  └───┘   └────────┘       └────┘   └──┘
par     └─────┘ └─────────┘  └─────┘   └────┘    └──┘  └───┘   └────────┘       └────┘   └──┘
pid            └─────────┘       └┘                                                
st     └─────────────────────────────┘└─────────────────────────────────┘└┘└──┘└────────────┘└┘
533  
534  end
535  
536  def list_equiv_of_equiv {α β : Type*} : α ≃ β → list α ≃ list β
id                                               └──┘   └──┘ 
src                                                 └──┘    └──┘
typ                                              └──┘   └──┘ 
doc                                                        
537  | ⟨f, g, l, r⟩ :=
538    by refine ⟨list.map f, list.map g, λ x, _, λ x, _⟩;
id                           └──────┘ 
src       └─────┘          └┘└──────┘ └┘ └─────┘ └────┘
typ       └─────┘         └┘└──────┘└┘ └─────┘ └────┘
doc       └─────┘          └┘         └┘ └─────┘ └────┘
txt       └─────┘          └┘         └┘ └─────┘ └────┘
par       └─────┘          └┘         └┘ └─────┘ └────┘
pid                       └┘         └┘ └─────┘ └────┘
st       └─────────────────────────────────────────────────
539       simp [id_of_left_inverse l, id_of_right_inverse r]
id              └────────────────┘   └─────────────────┘ 
src       └────┘└────────────────┘ └┘└─────────────────┘ └─
typ       └────┘└────────────────┘└┘└─────────────────┘└─
doc       └────┘                   └┘                    └─
txt       └────┘                   └┘                    └─
par       └────┘                   └┘                    └─
pid                              └┘                    
st   ────────────────────────────────────────────────────────
540  
src  
typ  
doc  
txt  
par  
pid  
st   
541  def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
id                                  └─┘         
src                                 └─┘           
typ                                 └─┘         
doc                                        
542  ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩
id                                     └─┘          └─┘
src                                           └─┘           └─┘
typ                                    └─┘          └─┘
543  
544  def decidable_eq_of_equiv [decidable_eq β] (e : α ≃ β) : decidable_eq α
id                              └──────────┘              └──────────┘ 
src                             └──────────┘                 └──────────┘
typ                             └──────────┘              └──────────┘ 
doc                                                    
545  | a₁ a₂ := decidable_of_iff (e a₁ = e a₂) e.injective.eq_iff
id     └┘ └┘    └──────────────┘            └────────┘└─────┘
src             └──────────────┘               └────────┘└─────┘
typ    └┘ └┘    └──────────────┘            └────────┘└─────┘
546  
547  def inhabited_of_equiv [inhabited β] (e : α ≃ β) : inhabited α :=
id                           └───────┘              └───────┘ 
src                          └───────┘                 └───────┘
typ                          └───────┘              └───────┘ 
doc                                              
548  ⟨e.symm (default _)⟩
id    └───┘  └─────┘
src    └───┘  └─────┘
typ   └───┘  └─────┘
549  
550  def unique_of_equiv (e : α ≃ β) (h : unique β) : unique α :=
id                                     └────┘     └────┘ 
src                                      └────┘      └────┘
typ                                    └────┘     └────┘ 
doc                             
551  unique.of_surjective e.symm.surjective
id   └──────────────────┘ └───┘└─────────┘
src  └──────────────────┘  └───┘└─────────┘
typ  └──────────────────┘ └───┘└─────────┘
552  
553  def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
id                               └────┘   └────┘ 
src                                └────┘    └────┘
typ                              └────┘   └────┘ 
doc                                         
554  { to_fun := e.symm.unique_of_equiv,
id               └───┘└──────────────┘
src               └───┘└──────────────┘
typ              └───┘└──────────────┘
555    inv_fun := e.unique_of_equiv,
id                └──────────────┘
src                └──────────────┘
typ               └──────────────┘
556    left_inv := λ _, subsingleton.elim _ _,
id                     └───────────────┘
src                     └───────────────┘
typ                    └───────────────┘
557    right_inv := λ _, subsingleton.elim _ _ }
id                      └───────────────┘
src                      └───────────────┘
typ                     └───────────────┘
558  
559  section
560  open subtype
561  
562  def subtype_congr {p : α → Prop} {q : β → Prop}
id                                        
typ                                       
563    (e : α ≃ β) (h : ∀ a, p a ↔ q (e a)) : {a : α // p a} ≃ {b : β // q b} :=
id                                                       
src                                                        
typ                                                      
doc                                                         
564  ⟨λ x, ⟨e x.1, (h _).1 x.2⟩,
id                   
src                       
typ                  
565   λ y, ⟨e.symm y.1, (h _).2 (by { simp, exact y.2 })⟩,
id         └───┘                            
src          └───┘                  └──┘  └────┘ └─┘
typ        └───┘                └──┘  └────┘└─┘
doc                                   └──┘  └────┘ └─┘
txt                                   └──┘  └────┘ └─┘
par                                   └──┘  └────┘ └─┘
pid                                               └─┘
st                                 └─────┘└──────────┘└┘
566   λ ⟨x, h⟩, subtype.eq' $ by simp,
id             └─────────┘
src             └─────────┘      └──┘
typ            └─────────┘      └──┘
doc                              └──┘
txt                              └──┘
par                              └──┘
st                              └───┘
567   λ ⟨y, h⟩, subtype.eq' $ by simp⟩
id             └─────────┘
src             └─────────┘      └──┘
typ            └─────────┘      └──┘
doc                              └──┘
txt                              └──┘
par                              └──┘
st                              └───┘
568  
569  def subtype_congr_right {p q : α → Prop} (e : ∀x, p x ↔ q x) : subtype p ≃ subtype q :=
id                                                           └─────┘   └─────┘ 
src                                                                └─────┘    └─────┘
typ                                                          └─────┘   └─────┘ 
doc                                                                           
570  subtype_congr (equiv.refl _) e
id   └───────────┘  └────────┘    
src  └───────────┘  └────────┘
typ  └───────────┘  └────────┘    
571  
572  @[simp] lemma subtype_congr_right_mk {p q : α → Prop} (e : ∀x, p x ↔ q x)
id                                                                    
src                                                                     
typ                                                                   
doc    └──┘
573    {x : α} (h : p x) : subtype_congr_right e ⟨x, h⟩ = ⟨x, (e x).1 h⟩ := rfl
id                      └─────────────────┘                     └─┘
src                        └─────────────────┘                            └─┘
typ                     └─────────────────┘                     └─┘
574  
575  def subtype_equiv_of_subtype' {p : α → Prop} (e : α ≃ β) :
id                                                      
src                                                      
typ                                                     
doc                                                      
576    {a : α // p a} ≃ {b : β // p (e.symm b)} :=
id                           └───┘ 
src                                └───┘
typ                          └───┘ 
doc                   
577  subtype_congr e $ by simp
id   └───────────┘ 
src  └───────────┘        └────
typ  └───────────┘       └────
doc                       └────
txt                       └────
par                       └────
pid                           
st                       └─────
578  
src  
typ  
doc  
txt  
par  
pid  
st   
579  def subtype_congr_prop {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
id                                                                 └─────┘   └─────┘ 
src                                                                   └─────┘    └─────┘
typ                                                                └─────┘   └─────┘ 
doc                                                                              
580  subtype_congr (equiv.refl α) (assume a, h ▸ iff.rfl)
id   └───────────┘  └────────┘               └─────┘
src  └───────────┘  └────────┘                  └─────┘
typ  └───────────┘  └────────┘               └─────┘
581  
582  def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
id                                    └─┘                
src                                   └─┘                   
typ                                   └─┘                
doc                                                          
583  subtype_congr_prop h
id   └────────────────┘ 
src  └────────────────┘
typ  └────────────────┘ 
584  
585  def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
id                                                                            └─────┘ 
src                                                                            └─────┘
typ                                                                           └─────┘ 
586    subtype q ≃ {a : α // ∃h:p a, q ⟨a, h⟩ } :=
id     └─────┘                   
src    └─────┘                  
typ    └─────┘                   
doc              
587  ⟨λ⟨⟨a, ha⟩, ha'⟩, ⟨a, ha, ha'⟩,
id        └┘   └─┘
typ       └┘   └─┘
588    λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by { cases ha, exact ha_h }⟩,
id        └┘          └───────┘                           └┘        └──┘
src                     └───────┘                        └────┘    └────┘    
typ       └┘          └───────┘                     └────┘└┘  └────┘└──┘
doc                                                      └────┘    └────┘    
txt                                                      └────┘    └────┘    
par                                                      └────┘    └────┘    
pid                                                                        
st                                                    └─────────┘└───────────┘└┘
589    assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
id                         └─┘                     └─┘
src                         └─┘                      └─┘
typ                        └─┘                     └─┘
590  
591  def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
id                                                               
typ                                                              
592    {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
id         └─────┘          └─────┘          
src        └─────┘             └─────┘           
typ        └─────┘          └─────┘          
doc                             
593  (subtype_subtype_equiv_subtype_exists p _).trans $
id    └──────────────────────────────────┘    └───┘
src   └──────────────────────────────────┘     └───┘
typ   └──────────────────────────────────┘    └───┘
594  subtype_congr_right $ λ x, exists_prop
id   └─────────────────┘       └─────────┘
src  └─────────────────┘        └─────────┘
typ  └─────────────────┘       └─────────┘
595  
596  /-- If the outer subtype has more restrictive predicate than the inner one,
597  then we can drop the latter. -/
598  def subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x}, q x → p x) :
id                                                                                  
typ                                                                                 
599    {x : subtype p // q x.1} ≃ subtype q :=
id         └─────┘          └─────┘ 
src        └─────┘             └─────┘
typ        └─────┘          └─────┘ 
doc                             
600  (subtype_subtype_equiv_subtype_inter p _).trans $
id    └─────────────────────────────────┘    └───┘
src   └─────────────────────────────────┘     └───┘
typ   └─────────────────────────────────┘    └───┘
601  subtype_congr_right $
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
602  assume x,
id          
typ         
603  ⟨and.right, λ h₁, ⟨h h₁, h₁⟩⟩
id    └───────┘    └┘    └┘  └┘
src   └───────┘
typ   └───────┘    └┘    └┘  └┘
604  
605  /-- If a proposition holds for all elements, then the subtype is
606  equivalent to the original type. -/
607  def subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ x, p x) :
id                                                               
typ                                                              
608    subtype p ≃ α :=
id     └─────┘   
src    └─────┘   
typ    └─────┘   
doc              
609  ⟨λ x, x, λ x, ⟨x, h x⟩, λ x, subtype.eq rfl, λ x, rfl⟩
id                         └────────┘ └─┘      └─┘
src                               └────────┘ └─┘       └─┘
typ                        └────────┘ └─┘      └─┘
610  
611  /-- A subtype of a sigma-type is a sigma-type over a subtype. -/
612  def subtype_sigma_equiv {α : Type u} (p : α → Type v) (q : α → Prop) :
id                                                             
typ                                                            
613    { y : sigma p // q y.1 } ≃ Σ(x : subtype q), p x.1 :=
id          └───┘                └─────┘    
src         └───┘                   └─────┘       
typ         └───┘                └─────┘    
doc                             
614  ⟨λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
id                   
src                      
typ                  
615   λ x, ⟨⟨x.1.1, x.2⟩, x.1.2⟩,
id                   
src                      
typ                  
616   λ ⟨⟨x, h⟩, y⟩, rfl,
id                  └─┘
src                  └─┘
typ                 └─┘
617   λ ⟨⟨x, y⟩, h⟩, rfl⟩
id                  └─┘
src                  └─┘
typ                 └─┘
618  
619  /-- A sigma type over a subtype is equivalent to the sigma set over the original type,
620  if the fiber is empty outside of the subset -/
621  def sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop)
id                                                                       
typ                                                                      
622    (h : ∀ x, p x → q x) :
id                   
typ                  
623    (Σ x : subtype q, p x) ≃ Σ x : α, p x :=
id           └─────┘             
src          └─────┘               
typ          └─────┘             
doc                           
624  (subtype_sigma_equiv p q).symm.trans $ subtype_univ_equiv $ λ x, h x.1 x.2
id    └─────────────────┘   └──┘ └───┘    └────────────────┘          
src   └─────────────────┘     └──┘ └───┘    └────────────────┘              
typ   └─────────────────┘   └──┘ └───┘    └────────────────┘          
doc   └─────────────────┘                   └────────────────┘
625  
626  def sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop)
id                                                                             
typ                                                                            
627    (h : ∀ x, p (f x)) :
id                 
typ                
628    (Σ y : subtype p, {x : α // f x = y}) ≃ α :=
id           └─────┘                 
src          └─────┘                     
typ          └─────┘                 
doc                                          
629  calc _ ≃ Σ y : β, {x : α // f x = y} : sigma_subtype_equiv_of_subset _ p (λ y ⟨x, h'⟩, h' ▸ h x)
id                                 └───────────────────────────┘          └┘       
src                                     └───────────────────────────┘                      
typ                                └───────────────────────────┘          └┘       
doc                                         └───────────────────────────┘
630     ... ≃ α                           : sigma_preimage_equiv f
id                                         └──────────────────┘ 
src                                         └──────────────────┘
typ                                        └──────────────────┘ 
631  
632  def sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β)
id                                                                              
typ                                                                             
633    {p : α → Prop} {q : β → Prop} (h : ∀ x, p x ↔ q (f x)) :
id                                                
src                                                
typ                                               
634    (Σ y : subtype q, {x : α // f x = y}) ≃ subtype p :=
id           └─────┘                 └─────┘ 
src          └─────┘                      └─────┘
typ          └─────┘                 └─────┘ 
doc                                          
635  calc (Σ y : subtype q, {x : α // f x = y}) ≃
id              └─────┘             
src             └─────┘                
typ             └─────┘             
636    Σ y : subtype q, {x : subtype p // subtype.mk (f x) ((h x).1 x.2) = y} :
id          └─────┘      └─────┘     └────────┘               
src         └─────┘       └─────┘      └────────┘                   
typ         └─────┘      └─────┘     └────────┘               
637    begin
st     └─────
638      apply sigma_congr_right,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
639      assume y,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
640      symmetry,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
st   ───────────┘└─
641      refine (subtype_subtype_equiv_subtype_exists _ _).trans (subtype_congr_right _),
id               └──────────────────────────────────┘             └─────────────────┘
src      └─────┘ └──────────────────────────────────┘└──────────┘ └─────────────────┘└─┘
typ      └─────┘ └──────────────────────────────────┘└──────────┘ └─────────────────┘└─┘
doc      └─────┘                                     └──────────┘                    └─┘
txt      └─────┘                                     └──────────┘                    └─┘
par      └─────┘                                     └──────────┘                    └─┘
pid                                                 └──────────┘                    └─┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
642      assume x,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
643      exact ⟨λ ⟨hp, h'⟩, congr_arg subtype.val h', λ h', ⟨(h x).2 (h'.symm ▸ y.2), subtype.eq h'⟩⟩
id                     └┘   └───────┘ └─────────┘                     └───┘       └────────┘
src      └────┘  └┘  └┘  └─┘└───────┘└─────────┘  └┘ └───┘    └──┘   └───┘ └───┘└────────┘  └──
typ      └────┘  └┘  └┘└┘└─┘└───────┘└─────────┘  └┘ └───┘  └──┘   └───┘└───┘└────────┘  └──
doc      └────┘  └┘  └┘  └─┘                      └┘ └───┘    └──┘          └───┘            └──
txt      └────┘  └┘  └┘  └─┘                      └┘ └───┘    └──┘          └───┘            └──
par      └────┘  └┘  └┘  └─┘                      └┘ └───┘    └──┘          └───┘            └──
pid             └┘  └┘  └─┘                      └┘ └───┘    └──┘          └───┘            └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
644    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
645  
646     ... ≃ subtype p : sigma_preimage_equiv (λ x : subtype p, (⟨f x, (h x).1 x.property⟩ : subtype q))
id            └─────┘    └──────────────────┘        └─────┘             └───────┘    └─────┘ 
src           └─────┘     └──────────────────┘        └─────┘                   └───────┘    └─────┘
typ           └─────┘    └──────────────────┘        └─────┘             └───────┘    └─────┘ 
647  
648  def pi_equiv_subtype_sigma (ι : Type*) (π : ι → Type*) :
id                                               
typ                                              
649    (Πi, π i) ≃ {f : ι → Σi, π i | ∀i, (f i).1 = i } :=
id                                 
src                                          
typ                                
doc              
650  ⟨ λf, ⟨λi, ⟨i, f i⟩, assume i, rfl⟩, λf i, begin rw ← f.2 i, exact (f.1 i).2 end,
id                            └─┘                                 
src                                 └─┘               └───┘ └─┘   └────┘  └─┘ └──┘
typ                           └─┘             └───┘└─┘  └────┘ └─┘└──┘
doc                                                   └───┘ └─┘   └────┘  └─┘ └──┘
txt                                                   └───┘ └─┘   └────┘  └─┘ └──┘
par                                                   └───┘ └─┘   └────┘  └─┘ └──┘
pid                                                     └─┘ └─┘          └─┘ └─┘
st                                              └──────────────┘└────────────────┘└─┘
651    assume f, funext $ assume i, rfl,
id              └────┘            └─┘
src              └────┘             └─┘
typ             └────┘            └─┘
652    assume ⟨f, hf⟩, subtype.eq $ funext $ assume i, sigma.eq (hf i).symm $
id               └┘   └────────┘   └────┘            └──────┘      └──┘
src                    └────────┘   └────┘             └──────┘       └──┘
typ              └┘   └────────┘   └────┘            └──────┘      └──┘
653      eq_of_heq $ rec_heq_of_heq _ $ rec_heq_of_heq _ $ heq.refl _⟩
id       └───────┘   └────────────┘     └────────────┘     └──────┘
src      └───────┘   └────────────┘     └────────────┘     └──────┘
typ      └───────┘   └────────────┘     └────────────┘     └──────┘
654  
655  def subtype_pi_equiv_pi {α : Sort u} {β : α → Sort v} {p : Πa, β a → Prop} :
id                                                                 
typ                                                                
656    {f : Πa, β a // ∀a, p a (f a) } ≃ Πa, { b : β a // p a b } :=
id                                            
src                                        
typ                                           
doc                                    
657  ⟨λf a, ⟨f.1 a, f.2 a⟩, λf, ⟨λa, (f a).1, λa, (f a).2⟩,
id                                     
src                                                 
typ                                    
658    by { rintro ⟨f, h⟩, refl },
src         └───────────┘  └───┘
typ         └───────────┘  └───┘
doc         └───────────┘  └───┘
txt         └───────────┘  └───┘
par         └───────────┘  └───┘
pid               └─────┘      
st       └──────────────┘└─────┘└┘
659    by { rintro f, funext a, exact subtype.eq' rfl }⟩
id                                    └─────────┘ └─┘
src         └──────┘  └──────┘  └────┘└─────────┘└─┘
typ         └──────┘  └──────┘  └────┘└─────────┘└─┘
doc         └──────┘  └──────┘  └────┘              
txt         └──────┘  └──────┘  └────┘              
par         └──────┘  └──────┘  └────┘              
pid               └┘        └┘                     
st       └─────────┘└────────┘└──────────────────────┘└┘
660  
661  end
662  
663  namespace set
664  open set
665  
666  protected def univ (α) : @univ α ≃ α :=
id                             └──┘   
src                            └──┘   
typ                            └──┘   
doc                                   
667  ⟨subtype.val, λ a, ⟨a, trivial⟩, λ ⟨a, _⟩, rfl, λ a, rfl⟩
id    └─────────┘         └─────┘            └─┘      └─┘
src   └─────────┘           └─────┘             └─┘       └─┘
typ   └─────────┘         └─────┘            └─┘      └─┘
668  
669  @[simp] lemma univ_apply {α : Type u} (x : @univ α) :
id                                               └──┘ 
src                                              └──┘
typ                                              └──┘ 
doc    └──┘
670    equiv.set.univ α x = x := rfl
id     └────────────┘        └─┘
src    └────────────┘           └─┘
typ    └────────────┘        └─┘
671  
672  @[simp] lemma univ_symm_apply {α : Type u} (x : α) :
id                                                   
typ                                                  
doc    └──┘
673    (equiv.set.univ α).symm x = ⟨x, trivial⟩ := rfl
id      └────────────┘  └──┘       └─────┘     └─┘
src     └────────────┘   └──┘         └─────┘     └─┘
typ     └────────────┘  └──┘       └─────┘     └─┘
674  
675  protected def empty (α) : (∅ : set α) ≃ empty :=
id                                 └─┘    └───┘
src                                └─┘     └───┘
typ                                └─┘    └───┘
doc                                        
676  equiv_empty $ λ ⟨x, h⟩, not_mem_empty x h
id   └─────────┘          └───────────┘
src  └─────────┘             └───────────┘
typ  └─────────┘          └───────────┘
677  
678  protected def pempty (α) : (∅ : set α) ≃ pempty :=
id                                  └─┘    └────┘
src                                 └─┘     └────┘
typ                                 └─┘    └────┘
doc                                          └────┘
679  equiv_pempty $ λ ⟨x, h⟩, not_mem_empty x h
id   └──────────┘          └───────────┘
src  └──────────┘             └───────────┘
typ  └──────────┘          └───────────┘
680  
681  protected def union' {α} {s t : set α}
id                                   └─┘ 
src                                  └─┘
typ                                  └─┘ 
682    (p : α → Prop) [decidable_pred p]
id                    └────────────┘ 
src                    └────────────┘
typ                   └────────────┘ 
683    (hs : ∀ x ∈ s, p x)
id                   
src            
typ                  
684    (ht : ∀ x ∈ t, ¬ p x) : (s ∪ t : set α) ≃ s ⊕ t :=
id                              └─┘      
src                                   └─┘       
typ                             └─┘      
doc                                            
685  { to_fun := λ x, if hp : p x.1
id                   └┘       
src                   └┘         
typ                  └┘       
686      then sum.inl ⟨_, x.2.resolve_right (λ xt, ht _ xt hp)⟩
id            └─────┘      └───────────┘     └┘  └┘   └┘ └┘
src           └─────┘       └───────────┘
typ           └─────┘      └───────────┘     └┘  └┘   └┘ └┘
687      else sum.inr ⟨_, x.2.resolve_left (λ xs, hp (hs _ xs))⟩,
id            └─────┘      └──────────┘     └┘  └┘  └┘   └┘
src           └─────┘       └──────────┘
typ           └─────┘      └──────────┘     └┘  └┘  └┘   └┘
688    inv_fun := λ o, match o with
id                          
typ                         
689      | (sum.inl x) := ⟨x.1, or.inl x.2⟩
id          └─────┘           └────┘  
src         └─────┘            └────┘  
typ         └─────┘           └────┘  
690      | (sum.inr x) := ⟨x.1, or.inr x.2⟩
id          └─────┘           └────┘  
src         └─────┘            └────┘  
typ         └─────┘           └────┘  
691    end,
692    left_inv := λ ⟨x, h'⟩, by by_cases p x; simp [union'._match_1, h]; congr,
id                                                └─────────────┘  
src                              └───────┘    └────┘               └┘   └───┘
typ                             └───────┘  └────┘└─────────────┘└┘  └───┘
doc                              └───────┘    └────┘               └┘ 
txt                              └───────┘    └────┘               └┘   └───┘
par                              └───────┘    └────┘               └┘   └───┘
pid                                                             └┘ 
st                              └─────────────────────────────────────────────┘
693    right_inv := λ o, begin
id                    
typ                   
st                       └─────
694      rcases o with ⟨x, h⟩ | ⟨x, h⟩;
id              
src      └─────┘ └───────────────────┘
typ      └─────┘└───────────────────┘
doc      └─────┘ └───────────────────┘
txt      └─────┘ └───────────────────┘
par      └─────┘ └───────────────────┘
pid             └───────────────────┘
st   ───────────────────────────────────
695      dsimp [union'._match_1];
id              └─────────────┘
src      └─────┘               
typ      └─────┘└─────────────┘
doc      └─────┘               
txt      └─────┘               
par      └─────┘               
pid                          
st   ─────────────────────────────
696      [simp [hs _ h], simp [ht _ h]]
id             └┘            └┘   
src      └────┘  └─┘   └────┘  └─┘ 
typ      └────┘└┘└─┘  └────┘└┘└─┘
doc       └────┘  └─┘   └────┘  └─┘ 
txt       └────┘  └─┘   └────┘  └─┘ 
par       └────┘  └─┘   └────┘  └─┘ 
pid             └─┘         └─┘ 
st   ─────────────────────────────────┘
697    end }
st   ────┘
698  
699  protected def union {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅) :
id                                  └─┘    └────────────┘            
src                                 └─┘     └────────────┘               
typ                                 └─┘    └────────────┘            
700    (s ∪ t : set α) ≃ s ⊕ t :=
id           └─┘      
src            └─┘       
typ          └─┘      
doc                    
701  set.union' s (λ _, id) (λ x xt xs, subset_empty_iff.2 H ⟨xs, xt⟩)
id   └────────┘       └┘      └┘ └┘  └──────────────┘    └┘  └┘
src  └────────┘         └┘              └──────────────┘
typ  └────────┘       └┘      └┘ └┘  └──────────────┘    └┘  └┘
702  
703  lemma union_apply_left {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅)
id                                     └─┘    └────────────┘            
src                                    └─┘     └────────────┘               
typ                                    └─┘    └────────────┘            
704    {a : (s ∪ t : set α)} (ha : ↑a ∈ s) : equiv.set.union H a = sum.inl ⟨a, ha⟩ :=
id                └─┘                └─────────────┘    └─────┘    └┘
src                 └─┘                   └─────────────┘      └─────┘
typ               └─┘                └─────────────┘    └─────┘    └┘
705  dif_pos ha
id   └─────┘ └┘
src  └─────┘
typ  └─────┘ └┘
706  
707  lemma union_apply_right {α} {s t : set α} [decidable_pred s] (H : s ∩ t = ∅)
id                                      └─┘    └────────────┘            
src                                     └─┘     └────────────┘               
typ                                     └─┘    └────────────┘            
708    {a : (s ∪ t : set α)} (ha : ↑a ∈ t) : equiv.set.union H a = sum.inr ⟨a, ha⟩ :=
id                └─┘                └─────────────┘    └─────┘    └┘
src                 └─┘                   └─────────────┘      └─────┘
typ               └─┘                └─────────────┘    └─────┘    └┘
709  dif_neg (show ↑a ∉ s, by finish [set.ext_iff])
id   └─────┘                      └─────────┘
src  └─────┘                └──────┘└─────────┘
typ  └─────┘              └──────┘└─────────┘
doc                           └──────┘           
txt                           └──────┘           
par                           └──────┘           
pid                                 └┘           
st                           └───────────────────┘
710  
711  protected def singleton {α} (a : α) : ({a} : set α) ≃ punit.{u} :=
id                                             └─┘    └───┘
src                                              └─┘     └───┘
typ                                            └─┘    └───┘
doc                                                      
712  ⟨λ _, punit.star, λ _, ⟨a, mem_singleton _⟩,
id        └────────┘         └───────────┘
src        └────────┘           └───────────┘
typ       └────────┘         └───────────┘
713   λ ⟨x, h⟩, by { simp at h, subst x },
id                                   
src                  └───────┘  └────┘ 
typ                 └───────┘  └────┘
doc                  └───────┘  └────┘ 
txt                  └───────┘  └────┘ 
par                  └───────┘  └────┘ 
pid                      └──┘        
st                └──────────┘└────────┘└┘
714   λ ⟨⟩, rfl⟩
id         └─┘
src        └─┘
typ        └─┘
715  
716  protected def of_eq {α : Type u} {s t : set α} (h : s = t) : s ≃ t :=
id                                           └─┘                
src                                          └─┘                   
typ                                          └─┘                
doc                                                                 
717  { to_fun := λ x, ⟨x.1, h ▸ x.2⟩,
id                         
src                            
typ                        
718    inv_fun := λ x, ⟨x.1, h.symm ▸ x.2⟩,
id                        └───┘  
src                          └───┘   
typ                       └───┘  
719    left_inv := λ _, subtype.eq rfl,
id                     └────────┘ └─┘
src                     └────────┘ └─┘
typ                    └────────┘ └─┘
720    right_inv := λ _, subtype.eq rfl }
id                      └────────┘ └─┘
src                      └────────┘ └─┘
typ                     └────────┘ └─┘
721  
722  @[simp] lemma of_eq_apply {α : Type u} {s t : set α} (h : s = t) (a : s) :
id                                                 └─┘                 
src                                                └─┘           
typ                                                └─┘                 
doc    └──┘
723    equiv.set.of_eq h a = ⟨a, h ▸ a.2⟩ := rfl
id     └─────────────┘               └─┘
src    └─────────────┘                    └─┘
typ    └─────────────┘               └─┘
724  
725  @[simp] lemma of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (a : t) :
id                                                      └─┘                 
src                                                     └─┘           
typ                                                     └─┘                 
doc    └──┘
726    (equiv.set.of_eq h).symm a = ⟨a, h.symm ▸ a.2⟩ := rfl
id      └─────────────┘  └──┘       └───┘        └─┘
src     └─────────────┘   └──┘          └───┘         └─┘
typ     └─────────────┘  └──┘       └───┘        └─┘
727  
728  protected def insert {α} {s : set.{u} α} [decidable_pred s] {a : α} (H : a ∉ s) :
id                                 └─┘        └────────────┘                 
src                                └─┘         └────────────┘                   
typ                                └─┘        └────────────┘                 
729    (insert a s : set α) ≃ s ⊕ punit.{u+1} :=
id      └────┘     └─┘      └───┘
src     └────┘       └─┘        └───┘
typ     └────┘     └─┘      └───┘
doc                         
730  calc (insert a s : set α) ≃ ↥(s ∪ {a}) : equiv.set.of_eq (by simp)
id         └────┘     └─┘             └─────────────┘
src        └────┘       └─┘                └─────────────┘     └──┘
typ        └────┘     └─┘             └─────────────┘     └──┘
doc                                                               └──┘
txt                                                               └──┘
par                                                               └──┘
st                                                               └───┘
731  ... ≃ s ⊕ ({a} : set α) : equiv.set.union (by finish [set.ext_iff])
id                └─┘     └─────────────┘             └─────────┘
src                 └─┘      └─────────────┘     └──────┘└─────────┘
typ               └─┘     └─────────────┘     └──────┘└─────────┘
doc                                                └──────┘           
txt                                                └──────┘           
par                                                └──────┘           
pid                                                      └┘           
st                                                └───────────────────┘
732  ... ≃ s ⊕ punit.{u+1} : sum_congr (equiv.refl _) (equiv.set.singleton _)
id           └───┘         └───────┘  └────────┘     └─────────────────┘
src           └───┘         └───────┘  └────────┘     └─────────────────┘
typ          └───┘         └───────┘  └────────┘     └─────────────────┘
733  
734  protected def sum_compl {α} (s : set α) [decidable_pred s] : s ⊕ (-s : set α) ≃ α :=
id                                    └─┘    └────────────┘           └─┘    
src                                   └─┘     └────────────┘              └─┘    
typ                                   └─┘    └────────────┘           └─┘    
doc                                                                                
735  calc s ⊕ (-s : set α) ≃ ↥(s ∪ -s) : (equiv.set.union (by simp [set.ext_iff])).symm
id              └─┘             └─────────────┘           └─────────┘   └──┘
src               └─┘                └─────────────┘     └────┘└─────────┘  └──┘
typ             └─┘             └─────────────┘     └────┘└─────────┘  └──┘
doc                                                           └────┘           
txt                                                           └────┘           
par                                                           └────┘           
pid                                                                          
st                                                           └─────────────────┘
736  ... ≃ @univ α : equiv.set.of_eq (by simp)
id          └──┘    └─────────────┘
src         └──┘     └─────────────┘     └──┘
typ         └──┘    └─────────────┘     └──┘
doc                                      └──┘
txt                                      └──┘
par                                      └──┘
st                                      └───┘
737  ... ≃ α : equiv.set.univ _
id            └────────────┘
src            └────────────┘
typ           └────────────┘
738  
739  @[simp] lemma sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred s] (x : s) :
id                                                       └─┘    └────────────┘        
src                                                      └─┘     └────────────┘
typ                                                      └─┘    └────────────┘        
doc    └──┘
740    equiv.set.sum_compl s (sum.inl x) = x := rfl
id     └─────────────────┘   └─────┘        └─┘
src    └─────────────────┘    └─────┘          └─┘
typ    └─────────────────┘   └─────┘        └─┘
741  
742  @[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred s] (x : -s) :
id                                                       └─┘    └────────────┘        
src                                                      └─┘     └────────────┘         
typ                                                      └─┘    └────────────┘        
doc    └──┘
743    equiv.set.sum_compl s (sum.inr x) = x := rfl
id     └─────────────────┘   └─────┘        └─┘
src    └─────────────────┘    └─────┘          └─┘
typ    └─────────────────┘   └─────┘        └─┘
744  
745  lemma sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
id                                                       └─┘    └────────────┘        
src                                                      └─┘     └────────────┘
typ                                                      └─┘    └────────────┘        
746    (hx : x ∈ s) : (equiv.set.sum_compl s).symm x = sum.inl ⟨x, hx⟩ :=
id                  └─────────────────┘  └──┘    └─────┘    └┘
src                   └─────────────────┘   └──┘     └─────┘
typ                 └─────────────────┘  └──┘    └─────┘    └┘
747  have ↑(⟨x, or.inl hx⟩ : (s ∪ -s : set α)) ∈ s, from hx,
id            └────┘ └┘          └─┘            └┘
src            └────┘               └─┘     
typ           └────┘ └┘          └─┘            └┘
748  by { rw [equiv.set.sum_compl], simpa using set.union_apply_left _ this }
id            └─────────────────┘               └──────────────────┘   └──┘
src       └──┘└─────────────────┘  └──────────┘└──────────────────┘└─┘    
typ       └──┘└─────────────────┘  └──────────┘└──────────────────┘└─┘└──┘
doc       └──┘                     └──────────┘                    └─┘    
txt       └──┘                     └──────────┘                    └─┘    
par       └──┘                     └──────────┘                    └─┘    
pid         └┘                          └────┘                    └─┘    
st     └────────────────────────┘└─────────────────────────────────────────┘└┘
749  
750  lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
id                                                           └─┘    └────────────┘        
src                                                          └─┘     └────────────┘
typ                                                          └─┘    └────────────┘        
751    (hx : x ∉ s) : (equiv.set.sum_compl s).symm x = sum.inr ⟨x, hx⟩ :=
id                  └─────────────────┘  └──┘    └─────┘    └┘
src                   └─────────────────┘   └──┘     └─────┘
typ                 └─────────────────┘  └──┘    └─────┘    └┘
752  have ↑(⟨x, or.inr hx⟩ : (s ∪ -s : set α)) ∈ -s, from hx,
id            └────┘ └┘          └─┘            └┘
src            └────┘               └─┘      
typ           └────┘ └┘          └─┘            └┘
753  by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
id            └─────────────────┘               └───────────────────┘   └──┘
src       └──┘└─────────────────┘  └──────────┘└───────────────────┘└─┘    
typ       └──┘└─────────────────┘  └──────────┘└───────────────────┘└─┘└──┘
doc       └──┘                     └──────────┘                     └─┘    
txt       └──┘                     └──────────┘                     └─┘    
par       └──┘                     └──────────┘                     └─┘    
pid         └┘                          └────┘                     └─┘    
st     └────────────────────────┘└──────────────────────────────────────────┘└┘
754  
755  protected def union_sum_inter {α : Type u} (s t : set α) [decidable_pred s] :
id                                                     └─┘    └────────────┘ 
src                                                    └─┘     └────────────┘
typ                                                    └─┘    └────────────┘ 
756    (s ∪ t : set α) ⊕ (s ∩ t : set α) ≃ s ⊕ t :=
id           └─┘          └─┘      
src            └─┘             └─┘       
typ          └─┘          └─┘      
doc                                      
757  calc  (s ∪ t : set α) ⊕ (s ∩ t : set α)
id               └─┘          └─┘ 
src                └─┘             └─┘
typ              └─┘          └─┘ 
758      ≃ (s ∪ t \ s : set α) ⊕ (s ∩ t : set α) : by rw [union_diff_self]
id                 └─┘          └─┘            └─────────────┘
src                   └─┘             └─┘         └──┘└─────────────┘└┘
typ                └─┘          └─┘        └──┘└─────────────┘└┘
doc                                                   └──┘               └┘
txt                                                   └──┘               └┘
par                                                   └──┘               └┘
pid                                                     └┘               
st                                                   └──────────────────┘
759  ... ≃ (s ⊕ (t \ s : set α)) ⊕ (s ∩ t : set α) :
id                  └─┘           └─┘ 
src                    └─┘              └─┘
typ                 └─┘           └─┘ 
760    sum_congr (set.union (inter_diff_self _ _)) (equiv.refl _)
id     └───────┘  └───────┘  └─────────────┘        └────────┘
src    └───────┘  └───────┘  └─────────────┘        └────────┘
typ    └───────┘  └───────┘  └─────────────┘        └────────┘
761  ... ≃ s ⊕ (t \ s : set α) ⊕ (s ∩ t : set α) : sum_assoc _ _ _
id                 └─┘          └─┘     └───────┘
src                   └─┘             └─┘      └───────┘
typ                └─┘          └─┘     └───────┘
762  ... ≃ s ⊕ (t \ s ∪ s ∩ t : set α) : sum_congr (equiv.refl _) begin
id                     └─┘     └───────┘  └────────┘
src                         └─┘      └───────┘  └────────┘
typ                    └─┘     └───────┘  └────────┘
st                                                                └─────
763      refine (set.union' (∉ s) _ _).symm,
id               └────────┘   
src      └─────┘ └────────┘└┘ └─────────┘
typ      └─────┘ └────────┘└┘└─────────┘
doc      └─────┘            └┘ └─────────┘
txt      └─────┘            └┘ └─────────┘
par      └─────┘            └┘ └─────────┘
pid                        └┘ └────────┘
st   ─────────────────────────────────────┘└─
764      exacts [λ x hx, hx.2, λ x hx, not_not_intro hx.1]
id                                     └───────────┘
src      └──────┘ └─────┘  └──┘ └─────┘└───────────┘  └───
typ      └──────┘ └─────┘  └──┘ └─────┘└───────────┘  └───
doc      └──────┘ └─────┘  └──┘ └─────┘               └───
txt      └──────┘ └─────┘  └──┘ └─────┘               └───
par      └──────┘ └─────┘  └──┘ └─────┘               └───
pid            └┘ └─────┘  └──┘ └─────┘               └─┘
st   ──────────────────────────────────────────────────────
765    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
766  ... ≃ s ⊕ t : by { rw (_ : t \ s ∪ s ∩ t = t), rw [union_comm, inter_comm, inter_union_diff] }
id                                             └────────┘  └────────┘  └──────────────┘
src                    └─┘ └──┘       └──┘└────────┘└┘└────────┘└┘└──────────────┘└┘
typ                  └─┘ └──┘     └──┘└────────┘└┘└────────┘└┘└──────────────┘└┘
doc                     └─┘ └──┘           └──┘          └┘          └┘                └┘
txt                     └─┘ └──┘           └──┘          └┘          └┘                └┘
par                     └─┘ └──┘           └──┘          └┘          └┘                └┘
pid                        └──┘             └┘          └┘          └┘                
st                   └───────────────────────────┘└──────────────┘└──────────┘└────────────────┘└┘
767  
768  protected def prod {α β} (s : set α) (t : set β) :
id                                 └─┘        └─┘ 
src                                └─┘         └─┘
typ                                └─┘        └─┘ 
769    s.prod t ≃ s × t :=
id     └───┘     
src     └───┘      
typ    └───┘     
doc     └───┘   
770  ⟨λp, ⟨⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩⟩,
id                        
src                            
typ                       
771   λp, ⟨⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩⟩,
id                        
src                            
typ                       
772   λ ⟨⟨x, y⟩, ⟨h₁, h₂⟩⟩, rfl,
id                         └─┘
src                         └─┘
typ                        └─┘
773   λ ⟨⟨x, h₁⟩, ⟨y, h₂⟩⟩, rfl⟩
id                         └─┘
src                         └─┘
typ                        └─┘
774  
775  protected noncomputable def image_of_inj_on {α β} (f : α → β) (s : set α) (H : inj_on f s) :
id                                                                    └─┘        └────┘  
src                                                                     └─┘         └────┘
typ                                                                   └─┘        └────┘  
doc                                                                                 └────┘
776    s ≃ (f '' s) :=
id         └┘ 
src          └┘
typ        └┘ 
doc      
777  ⟨λ ⟨x, h⟩, ⟨f x, mem_image_of_mem f h⟩,
id                └──────────────┘ 
src                   └──────────────┘
typ               └──────────────┘ 
778   λ ⟨y, h⟩, ⟨classical.some h, (classical.some_spec h).1⟩,
id             └────────────┘     └─────────────────┘   
src              └────────────┘     └─────────────────┘   
typ            └────────────┘     └─────────────────┘   
779   λ ⟨x, h⟩, subtype.eq (H (classical.some_spec (mem_image_of_mem f h)).1 h
id            └────────┘    └─────────────────┘  └──────────────┘     
src             └────────┘     └─────────────────┘  └──────────────┘      
typ           └────────┘    └─────────────────┘  └──────────────┘     
780     (classical.some_spec (mem_image_of_mem f h)).2),
id       └─────────────────┘  └──────────────┘     
src      └─────────────────┘  └──────────────┘      
typ      └─────────────────┘  └──────────────┘     
781   λ ⟨y, h⟩, subtype.eq (classical.some_spec h).2⟩
id            └────────┘  └─────────────────┘   
src             └────────┘  └─────────────────┘   
typ           └────────┘  └─────────────────┘   
782  
783  protected noncomputable def image {α β} (f : α → β) (s : set α) (H : injective f) : s ≃ (f '' s) :=
id                                                          └─┘        └───────┘         └┘ 
src                                                           └─┘         └───────┘            └┘
typ                                                         └─┘        └───────┘         └┘ 
doc                                                                                        
784  equiv.set.image_of_inj_on f s (λ x y hx hy hxy, H hxy)
id   └───────────────────────┘        └┘ └┘ └─┘   └─┘
src  └───────────────────────┘
typ  └───────────────────────┘        └┘ └┘ └─┘   └─┘
785  
786  @[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) :
id                                                    └─┘        └───────┘ 
src                                                     └─┘         └───────┘
typ                                                   └─┘        └───────┘ 
doc    └──┘
787    set.image f s H ⟨a, h⟩ = ⟨f a, mem_image_of_mem _ h⟩ := rfl
id     └───────┘              └──────────────┘        └─┘
src    └───────┘                     └──────────────┘         └─┘
typ    └───────┘              └──────────────┘        └─┘
788  
789  protected noncomputable def range {α β} (f : α → β) (H : injective f) :
id                                                          └───────┘ 
src                                                           └───────┘
typ                                                         └───────┘ 
790    α ≃ range f :=
id       └───┘ 
src       └───┘
typ      └───┘ 
doc       └───┘
791  { to_fun := λ x, ⟨f x, mem_range_self _⟩,
id                       └────────────┘
src                         └────────────┘
typ                      └────────────┘
792    inv_fun := λ x, classical.some x.2,
id                    └────────────┘ 
src                    └────────────┘  
typ                   └────────────┘ 
793    left_inv := λ x, H (classical.some_spec (show f x ∈ range f, from mem_range_self _)),
id                       └─────────────────┘          └───┘        └────────────┘
src                        └─────────────────┘            └───┘         └────────────┘
typ                      └─────────────────┘          └───┘        └────────────┘
doc                                                        └───┘
794    right_inv := λ x, subtype.eq $ classical.some_spec x.2 }
id                      └────────┘   └─────────────────┘ 
src                      └────────┘   └─────────────────┘  
typ                     └────────┘   └─────────────────┘ 
795  
796  @[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
id                                                    └───────┘ 
src                                                     └───────┘
typ                                                   └───────┘ 
doc    └──┘
797    set.range f H a = ⟨f a, set.mem_range_self _⟩ := rfl
id     └───────┘         └────────────────┘       └─┘
src    └───────┘              └────────────────┘       └─┘
typ    └───────┘         └────────────────┘       └─┘
798  
799  protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
id                                                └─┘   └─┘ 
src                                                 └─┘    └─┘
typ                                               └─┘   └─┘ 
doc                                                       
800  ⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
id         └┘       └───┘ └┘   └──────────────┘   └──────────────┘ └───┘
src          └┘          └───┘ └┘    └──────────────┘    └──────────────┘  └───┘
typ        └┘       └───┘ └┘   └──────────────┘   └──────────────┘ └───┘
801  
802  protected def sep {α : Type u} (s : set α) (t : α → Prop) :
id                                       └─┘        
src                                      └─┘
typ                                      └─┘        
803    ({ x ∈ s | t x } : set α) ≃ { x : s | t x.1 } :=
id                    └─┘             
src                      └─┘                 
typ                   └─┘             
doc                              
804  (equiv.subtype_subtype_equiv_subtype_inter s t).symm
id    └───────────────────────────────────────┘   └──┘
src   └───────────────────────────────────────┘     └──┘
typ   └───────────────────────────────────────┘   └──┘
805  
806  end set
807  
808  noncomputable def of_bijective {α β} {f : α → β} (hf : bijective f) : α ≃ β :=
id                                                        └───────┘       
src                                                         └───────┘        
typ                                                       └───────┘       
doc                                                                          
809  ⟨f, λ x, classical.some (hf.2 x), λ x, hf.1 (classical.some_spec (hf.2 (f x))),
id          └────────────┘  └┘         └┘   └─────────────────┘  └┘    
src           └────────────┘                    └─────────────────┘    
typ         └────────────┘  └┘         └┘   └─────────────────┘  └┘    
810    λ x, classical.some_spec (hf.2 x)⟩
id         └─────────────────┘  └┘  
src         └─────────────────┘    
typ        └─────────────────┘  └┘  
811  
812  @[simp] theorem of_bijective_to_fun {α β} {f : α → β} (hf : bijective f) : (of_bijective hf : α → β) = f := rfl
id                                                             └───────┘      └──────────┘ └┘             └─┘
src                                                              └───────┘       └──────────┘                   └─┘
typ                                                            └───────┘      └──────────┘ └┘             └─┘
doc    └──┘
813  
814  def subtype_quotient_equiv_quotient_subtype (p₁ : α → Prop) [s₁ : setoid α]
id                                                                    └────┘ 
src                                                                    └────┘
typ                                                                   └────┘ 
815    [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) (hp₂ :  ∀ a, p₁ a ↔ p₂ ⟦a⟧)
id           └────┘  └─────┘ └┘         └──────┘ └┘                     └┘   └┘ 
src          └────┘  └─────┘            └──────┘                                   
typ          └────┘  └─────┘ └┘         └──────┘ └┘                     └┘   └┘ 
816    (h : ∀ x y : subtype p₁, @setoid.r _ s₂ x y ↔ (x : α) ≈ y) :
id                  └─────┘ └┘   └──────┘   └┘           
src                 └─────┘      └──────┘                   
typ                 └─────┘ └┘   └──────┘   └┘           
817    {x // p₂ x} ≃ quotient s₂ :=
id         └┘    └──────┘ └┘
src                └──────┘
typ        └┘    └──────┘ └┘
doc                
818  { to_fun := λ a, quotient.hrec_on a.1 (λ a h, ⟦⟨a, (hp₂ _).2 h⟩⟧)
id                   └──────────────┘             └─┘      
src                   └──────────────┘                           
typ                  └──────────────┘             └─┘      
819      (λ a b hab, hfunext (by rw quotient.sound hab)
id            └─┘  └─────┘        └────────────┘ └─┘
src                  └─────┘     └─┘└────────────┘
typ           └─┘  └─────┘     └─┘└────────────┘└─┘
doc                              └─┘              
txt                              └─┘              
par                              └─┘              
pid                                              
st                              └────────────────────┘
820      (λ h₁ h₂ _, heq_of_eq (quotient.sound ((h _ _).2 hab)))) a.2,
id          └┘ └┘   └───────┘  └────────────┘          └─┘     
src                  └───────┘  └────────────┘                    
typ         └┘ └┘   └───────┘  └────────────┘          └─┘     
821    inv_fun := λ a, quotient.lift_on a (λ a, (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : {x // p₂ x}))
id                    └──────────────┘             └─┘              └┘ 
src                    └──────────────┘                              
typ                   └──────────────┘             └─┘              └┘ 
822      (λ a b hab, subtype.eq' (quotient.sound ((h _ _).1 hab))),
id            └─┘  └─────────┘  └────────────┘          └─┘
src                  └─────────┘  └────────────┘         
typ           └─┘  └─────────┘  └────────────┘          └─┘
823    left_inv := λ ⟨a, ha⟩, quotient.induction_on a (λ a ha, rfl) ha,
id                     └┘   └───────────────────┘       └┘  └─┘
src                           └───────────────────┘            └─┘
typ                    └┘   └───────────────────┘       └┘  └─┘
824    right_inv := λ a, quotient.induction_on a (λ ⟨a, ha⟩, rfl) }
id                      └───────────────────┘             └─┘
src                      └───────────────────┘               └─┘
typ                     └───────────────────┘             └─┘
825  
826  section swap
827  variable [decidable_eq α]
id             └──────────┘
src            └──────────┘
typ            └──────────┘
828  open decidable
829  
830  def swap_core (a b r : α) : α :=
id                              
typ                             
831  if r = a then b
id              
src       
typ             
832  else if r = b then a
id                   
src            
typ                  
833  else r
id        
typ       
834  
835  theorem swap_core_self (r a : α) : swap_core a a r = r :=
id                                     └───────┘     
src                                     └───────┘       
typ                                    └───────┘     
836  by { unfold swap_core, split_ifs; cc }
src       └──────────────┘  └───────┘  └─┘
typ       └──────────────┘  └───────┘  └─┘
doc       └──────────────┘  └───────┘  └─┘
txt       └──────────────┘  └───────┘  └─┘
par       └──────────────┘  └───────┘  └─┘
pid             └────────┘               
st     └─────────────────┘└──────────────┘└┘
837  
838  theorem swap_core_swap_core (r a b : α) : swap_core a b (swap_core a b r) = r :=
id                                            └───────┘    └───────┘      
src                                            └───────┘      └───────┘        
typ                                           └───────┘    └───────┘      
839  by { unfold swap_core, split_ifs; cc }
src       └──────────────┘  └───────┘  └─┘
typ       └──────────────┘  └───────┘  └─┘
doc       └──────────────┘  └───────┘  └─┘
txt       └──────────────┘  └───────┘  └─┘
par       └──────────────┘  └───────┘  └─┘
pid             └────────┘               
st     └─────────────────┘└──────────────┘└┘
840  
841  theorem swap_core_comm (r a b : α) : swap_core a b r = swap_core b a r :=
id                                       └───────┘     └───────┘   
src                                       └───────┘        └───────┘
typ                                      └───────┘     └───────┘   
842  by { unfold swap_core, split_ifs; cc }
src       └──────────────┘  └───────┘  └─┘
typ       └──────────────┘  └───────┘  └─┘
doc       └──────────────┘  └───────┘  └─┘
txt       └──────────────┘  └───────┘  └─┘
par       └──────────────┘  └───────┘  └─┘
pid             └────────┘               
st     └─────────────────┘└──────────────┘└┘
843  
844  /-- `swap a b` is the permutation that swaps `a` and `b` and
845    leaves other values as is. -/
846  def swap (a b : α) : perm α :=
id                       └──┘ 
src                       └──┘
typ                      └──┘ 
doc                       └──┘
847  ⟨swap_core a b, swap_core a b, λr, swap_core_swap_core r a b, λr, swap_core_swap_core r a b⟩
id    └───────┘    └───────┘       └─────────────────┘        └─────────────────┘   
src   └───────┘      └───────┘          └─────────────────┘            └─────────────────┘
typ   └───────┘    └───────┘       └─────────────────┘        └─────────────────┘   
848  
849  theorem swap_self (a : α) : swap a a = equiv.refl _ :=
id                              └──┘    └────────┘
src                              └──┘      └────────┘
typ                             └──┘    └────────┘
doc                              └──┘
850  eq_of_to_fun_eq $ funext $ λ r, swap_core_self r a
id   └─────────────┘   └────┘       └────────────┘  
src  └─────────────┘   └────┘        └────────────┘
typ  └─────────────┘   └────┘       └────────────┘  
851  
852  theorem swap_comm (a b : α) : swap a b = swap b a :=
id                                └──┘    └──┘  
src                                └──┘      └──┘
typ                               └──┘    └──┘  
doc                                └──┘       └──┘
853  eq_of_to_fun_eq $ funext $ λ r, swap_core_comm r _ _
id   └─────────────┘   └────┘       └────────────┘ 
src  └─────────────┘   └────┘        └────────────┘
typ  └─────────────┘   └────┘       └────────────┘ 
854  
855  theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
id                                       └──┘                                       
src                                       └──┘                                 
typ                                      └──┘                                       
doc                                       └──┘
856  rfl
id   └─┘
src  └─┘
typ  └─┘
857  
858  @[simp] theorem swap_apply_left (a b : α) : swap a b a = b :=
id                                              └──┘     
src                                              └──┘       
typ                                             └──┘     
doc    └──┘                                      └──┘
859  if_pos rfl
id   └────┘ └─┘
src  └────┘ └─┘
typ  └────┘ └─┘
860  
861  @[simp] theorem swap_apply_right (a b : α) : swap a b b = a :=
id                                               └──┘     
src                                               └──┘       
typ                                              └──┘     
doc    └──┘                                       └──┘
862  by { by_cases b = a; simp [swap_apply_def, *] }
id                           └────────────┘
src       └───────┘    └────┘└────────────┘└───┘
typ       └───────┘  └────┘└────────────┘└───┘
doc       └───────┘     └────┘              └───┘
txt       └───────┘     └────┘              └───┘
par       └───────┘     └────┘              └───┘
pid                                      └──┘
st     └──────────────────────────────────────────┘└┘
863  
864  theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x = x :=
id                                                         └──┘     
src                                                             └──┘       
typ                                                        └──┘     
doc                                                               └──┘
865  by simp [swap_apply_def] {contextual := tt}
id            └────────────┘                 └┘
src     └────┘└────────────┘└┘ └────────────┘└┘└─
typ     └────┘└────────────┘└┘ └────────────┘└┘└─
doc     └────┘              └┘ └────────────┘  └─
txt     └────┘              └┘ └────────────┘  └─
par     └────┘              └┘ └────────────┘  └─
pid                        └────────────┘  
st     └─────────────────────────────────────────
866  
src  
typ  
doc  
txt  
par  
pid  
st   
867  @[simp] theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
id                                         └──┘   └───┘   └──┘     └────────┘
src                                         └──┘     └───┘   └──┘       └────────┘
typ                                        └──┘   └───┘   └──┘     └────────┘
doc    └──┘                                 └──┘             └──┘
868  eq_of_to_fun_eq $ funext $ λ x, swap_core_swap_core _ _ _
id   └─────────────┘   └────┘       └─────────────────┘
src  └─────────────┘   └────┘        └─────────────────┘
typ  └─────────────┘   └────┘       └─────────────────┘
869  
870  theorem swap_comp_apply {a b x : α} (π : perm α) :
id                                           └──┘ 
src                                           └──┘
typ                                          └──┘ 
doc                                           └──┘
871    π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x :=
id     └────┘  └──┘                                           
src     └────┘  └──┘                                      
typ    └────┘  └──┘                                           
doc             └──┘
872  by { cases π, refl }
id              
src       └────┘   └───┘
typ       └────┘  └───┘
doc       └────┘   └───┘
txt       └────┘   └───┘
par       └────┘   └───┘
pid                   
st     └────────┘└─────┘└┘
873  
874  @[simp] lemma swap_inv {α : Type*} [decidable_eq α] (x y : α) :
id                                       └──────────┘          
src                                      └──────────┘
typ                                      └──────────┘          
doc    └──┘
875    (swap x y)⁻¹ = swap x y := rfl
id      └──┘   └┘  └──┘      └─┘
src     └──┘     └┘  └──┘        └─┘
typ     └──┘   └┘  └──┘      └─┘
doc     └──┘          └──┘
876  
877  @[simp] lemma symm_trans_swap_trans [decidable_eq β] (a b : α)
id                                        └──────────┘          
src                                       └──────────┘
typ                                       └──────────┘          
doc    └──┘
878    (e : α ≃ β) : (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
id                 └───┘└────┘  └──┘    └───┘    └──┘       
src                   └───┘└────┘  └──┘      └───┘     └──┘
typ                └───┘└────┘  └──┘    └───┘    └──┘       
doc                                └──┘                 └──┘
879  equiv.ext _ _ (λ x, begin
id   └───────┘        
src  └───────┘
typ  └───────┘        
st                       └─────
880    have : ∀ a, e.symm x = a ↔ x = e a :=
id                 └────┘          
src    └─────┘ └┘ └────┘      └───
typ    └─────┘ └┘ └────┘    └───
doc    └─────┘ └┘               └───
txt    └─────┘ └┘               └───
par    └─────┘ └┘               └───
pid    └───┘└┘ └┘               └───
st   ────────────────────────────────────────
881      λ a, by { rw @eq_comm _ (e.symm x), split; intros; simp * at * },
id                     └─────┘    └────┘ 
src  ───┘ └──┘  └─┘└─┘ └─────┘└─┘ └────┘ └┘└───┘└┘└────┘└┘└──────────┘
typ  ───┘ └──┘  └─┘└─┘ └─────┘└─┘ └────┘└┘└───┘└┘└────┘└┘└──────────┘
doc  ───┘ └──┘  └─┘└─┘        └─┘        └┘└───┘└┘└────┘└┘└──────────┘
txt  ───┘ └──┘  └─┘└─┘        └─┘        └┘└───┘└┘└────┘└┘└──────────┘
par  ───┘ └──┘  └─┘└─┘        └─┘        └┘└───┘└┘└────┘└┘└──────────┘
pid  ───┘ └──┘  └────┘        └─┘        └─────────────────────────────┘
st   ──────────┘└─────────────────────────┘└───────────────────────────┘└┘
882    simp [swap_apply_def, this],
id           └────────────┘  └──┘
src    └────┘└────────────┘└┘    
typ    └────┘└────────────┘└┘└──┘
doc    └────┘              └┘    
txt    └────┘              └┘    
par    └────┘              └┘    
pid                      └┘    
st   ────────────────────────────┘└─
883    split_ifs; simp
src    └───────┘  └───┘
typ    └───────┘  └───┘
doc    └───────┘  └───┘
txt    └───────┘  └───┘
par    └───────┘  └───┘
pid                   
st   ─────────────────┘
884  end)
st   └─┘
885  
886  @[simp] lemma swap_mul_self {α : Type*} [decidable_eq α] (i j : α) : swap i j * swap i j = 1 :=
id                                            └──────────┘              └──┘    └──┘   
src                                           └──────────┘                └──┘      └──┘     
typ                                           └──────────┘              └──┘    └──┘   
doc    └──┘                                                               └──┘       └──┘
887  equiv.swap_swap i j
id   └─────────────┘  
src  └─────────────┘
typ  └─────────────┘  
888  
889  @[simp] lemma swap_apply_self {α : Type*} [decidable_eq α] (i j a : α) : swap i j (swap i j a) = a :=
id                                              └──────────┘                └──┘    └──┘      
src                                             └──────────┘                  └──┘      └──┘        
typ                                             └──────────┘                └──┘    └──┘      
doc    └──┘                                                                   └──┘      └──┘
890  by rw [← perm.mul_apply, swap_mul_self, perm.one_apply]
id            └────────────┘  └───────────┘  └────────────┘
src     └────┘└────────────┘└┘└───────────┘└┘└────────────┘└─
typ     └────┘└────────────┘└┘└───────────┘└┘└────────────┘└─
doc     └────┘              └┘             └┘              └─
txt     └────┘              └┘             └┘              └─
par     └────┘              └┘             └┘              └─
pid       └──┘              └┘             └┘              
st     └───────────────────┘└─────────────┘└──────────────┘
891  
src  
typ  
doc  
txt  
par  
pid  
st   
892  /-- Augment an equivalence with a prescribed mapping `f a = b` -/
893  def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
id                                            
src                                               
typ                                           
doc                                               
894  (swap a (f.symm b)).trans f
id    └──┘   └───┘   └───┘  
src   └──┘     └───┘    └───┘
typ   └──┘   └───┘   └───┘  
doc   └──┘
895  
896  @[simp] theorem set_value_eq (f : α ≃ β) (a : α) (b : β) : set_value f a b a = b :=
id                                                         └───────┘      
src                                                            └───────┘         
typ                                                        └───────┘      
doc    └──┘                                                    └───────┘
897  by { dsimp [set_value], simp [swap_apply_left] }
id               └───────┘         └─────────────┘
src       └─────┘└───────┘  └────┘└─────────────┘└┘
typ       └─────┘└───────┘  └────┘└─────────────┘└┘
doc       └─────┘└───────┘  └────┘               └┘
txt       └─────┘           └────┘               └┘
par       └─────┘           └────┘               └┘
pid                                          
st     └──────────────────┘└───────────────────────┘└┘
898  
899  end swap
900  
901  protected lemma forall_congr {p : α → Prop} {q : β → Prop} (f : α ≃ β)
id                                                                   
src                                                                    
typ                                                                  
doc                                                                    
902    (h : ∀{x}, p x ↔ q (f x)) : (∀x, p x) ↔ (∀y, q y) :=
id                                       
src                                         
typ                                      
903  begin
st   └─────
904    split; intros h₂ x,
src    └───┘  └─────────┘
typ    └───┘  └─────────┘
doc    └───┘  └─────────┘
txt    └───┘  └─────────┘
par    └───┘  └─────────┘
pid                 └───┘
st   ───────────────────┘└─
905    { rw [←f.right_inv x], apply h.mp, apply h₂ },
id            └─────────┘ 
src      └───┘└─────────┘   └────┘      └────┘  
typ      └───┘└─────────┘  └────┘      └────┘  
doc      └───┘              └────┘      └────┘  
txt      └───┘              └────┘      └────┘  
par      └───┘              └────┘      └────┘  
pid        └─┘                                
st   ───┘└────────────────┘└───────────┘└─────────┘└┘
906    apply h.mpr, apply h₂
src    └────┘       └────┘  
typ    └────┘       └────┘  
doc    └────┘       └────┘  
txt    └────┘       └────┘  
par    └────┘       └────┘  
pid                       
st   ────────────┘└─────────┘
907  end
st   └─┘
908  
909  end equiv
910  
911  instance {α} [subsingleton α] : subsingleton (ulift α) := equiv.ulift.subsingleton
id                 └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
src                └──────────┘      └──────────┘  └───┘       └─────────┘└───────────┘
typ                └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
doc                                                └───┘
912  instance {α} [subsingleton α] : subsingleton (plift α) := equiv.plift.subsingleton
id                 └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
src                └──────────┘      └──────────┘  └───┘       └─────────┘└───────────┘
typ                └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
doc                                                └───┘
913  
914  instance {α} [decidable_eq α] : decidable_eq (ulift α) := equiv.ulift.decidable_eq
id                 └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
src                └──────────┘      └──────────┘  └───┘       └─────────┘└───────────┘
typ                └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
doc                                                └───┘
915  instance {α} [decidable_eq α] : decidable_eq (plift α) := equiv.plift.decidable_eq
id                 └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
src                └──────────┘      └──────────┘  └───┘       └─────────┘└───────────┘
typ                └──────────┘     └──────────┘  └───┘      └─────────┘└───────────┘
doc                                                └───┘
916  
917  def unique_unique_equiv : unique (unique α) ≃ unique α :=
id                             └────┘  └────┘    └────┘ 
src                            └────┘  └────┘     └────┘
typ                            └────┘  └────┘    └────┘ 
doc                                              
918  { to_fun := λ h, h.default,
id                   └──────┘
src                    └──────┘
typ                  └──────┘
919    inv_fun := λ h, { default := h, uniq := λ _, subsingleton.elim _ _ },
id                                               └───────────────┘
src                                                 └───────────────┘
typ                                              └───────────────┘
920    left_inv := λ _, subsingleton.elim _ _,
id                     └───────────────┘
src                     └───────────────┘
typ                    └───────────────┘
921    right_inv := λ _, subsingleton.elim _ _ }
id                      └───────────────┘
src                      └───────────────┘
typ                     └───────────────┘
922  
923  def equiv_of_unique_of_unique [unique α] [unique β] : α ≃ β :=
id                                  └────┘    └────┘       
src                                 └────┘     └────┘        
typ                                 └────┘    └────┘       
doc                                                          
924  { to_fun := λ _, default β,
id                   └─────┘ 
src                   └─────┘
typ                  └─────┘ 
925    inv_fun := λ _, default α,
id                    └─────┘ 
src                    └─────┘
typ                   └─────┘ 
926    left_inv := λ _, subsingleton.elim _ _,
id                     └───────────────┘
src                     └───────────────┘
typ                    └───────────────┘
927    right_inv := λ _, subsingleton.elim _ _ }
id                      └───────────────┘
src                      └───────────────┘
typ                     └───────────────┘
928  
929  def equiv_punit_of_unique [unique α] : α ≃ punit.{v} :=
id                              └────┘       └───┘
src                             └────┘         └───┘
typ                             └────┘       └───┘
doc                                           
930  equiv_of_unique_of_unique
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
931  
932  namespace quot
933  
934  /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
935  if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
936  protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
id                                                                  
src                                                                     
typ                                                                 
doc                                                                     
937    (eq : ∀a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
id            └┘ └┘  └┘ └┘ └┘  └┘   └┘    └┘
src                           
typ           └┘ └┘  └┘ └┘ └┘  └┘   └┘    └┘
938    quot ra ≃ quot rb :=
id     └──┘ └┘  └──┘ └┘
src            
typ    └──┘ └┘  └──┘ └┘
doc            
939  { to_fun := quot.map e (assume a₁ a₂, (eq a₁ a₂).1),
id               └──────┘          └┘ └┘   └┘ └┘ └┘ 
src              └──────┘                   └┘       
typ              └──────┘          └┘ └┘   └┘ └┘ └┘ 
doc              └──────┘
940    inv_fun := quot.map e.symm
id                └──────┘ └───┘
src               └──────┘  └───┘
typ               └──────┘ └───┘
doc               └──────┘
941      (assume b₁ b₂ h,
id               └┘ └┘ 
typ              └┘ └┘ 
942       (eq (e.symm b₁) (e.symm b₂)).2
id         └┘  └───┘ └┘   └───┘ └┘  
src        └┘   └───┘       └───┘     
typ        └┘  └───┘ └┘   └───┘ └┘  
943         ((e.apply_symm_apply b₁).symm ▸ (e.apply_symm_apply b₂).symm ▸ h)),
id            └───────────────┘ └┘ └──┘    └───────────────┘ └┘ └──┘   
src            └───────────────┘    └──┘     └───────────────┘    └──┘  
typ           └───────────────┘ └┘ └──┘    └───────────────┘ └┘ └──┘   
944    left_inv := by { rintros ⟨a⟩, dunfold quot.map, simp only [equiv.symm_apply_apply] },
id                                                                └────────────────────┘
src                     └─────────┘  └──────────────┘  └─────────┘└────────────────────┘└┘
typ                     └─────────┘  └──────────────┘  └─────────┘└────────────────────┘└┘
doc                     └─────────┘  └──────────────┘  └─────────┘                      └┘
txt                     └─────────┘  └──────────────┘  └─────────┘                      └┘
par                     └─────────┘  └──────────────┘  └─────────┘                      └┘
pid                            └──┘         └───────┘      └──┘└┘                      
st                   └────────────┘└────────────────┘└───────────────────────────────────┘└┘
945    right_inv := by { rintros ⟨a⟩, dunfold quot.map, simp only [equiv.apply_symm_apply] } }
id                                                                 └────────────────────┘
src                      └─────────┘  └──────────────┘  └─────────┘└────────────────────┘└┘
typ                      └─────────┘  └──────────────┘  └─────────┘└────────────────────┘└┘
doc                      └─────────┘  └──────────────┘  └─────────┘                      └┘
txt                      └─────────┘  └──────────────┘  └─────────┘                      └┘
par                      └─────────┘  └──────────────┘  └─────────┘                      └┘
pid                             └──┘         └───────┘      └──┘└┘                      
st                    └────────────┘└────────────────┘└───────────────────────────────────┘└┘
946  
947  /-- Quotients are congruent on equivalences under equality of their relation.
948  An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
949  protected def congr_right {r r' : α → α → Prop} (eq : ∀a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
id                                                        └┘ └┘   └┘ └┘  └┘ └┘ └┘
src                                                                        
typ                                                       └┘ └┘   └┘ └┘  └┘ └┘ └┘
950    quot r ≃ quot r' :=
id     └──┘   └──┘ └┘
src           
typ    └──┘   └──┘ └┘
doc           
951  quot.congr (equiv.refl α) eq
id   └────────┘  └────────┘   └┘
src  └────────┘  └────────┘    └┘
typ  └────────┘  └────────┘   └┘
doc  └────────┘
952  
953  /-- An equivalence `e : α ≃ β` generates an equivalence between the quotient space of `α`
954  by a relation `ra` and the quotient space of `β` by the image of this relation under `e`. -/
955  protected def congr_left {r : α → α → Prop} (e : α ≃ β) :
id                                                    
src                                                     
typ                                                   
doc                                                     
956    quot r ≃ quot (λ b b', r (e.symm b) (e.symm b')) :=
id     └──┘   └──┘     └┘    └───┘    └───┘ └┘
src                              └───┘      └───┘
typ    └──┘   └──┘     └┘    └───┘    └───┘ └┘
doc           
957  @quot.congr α β r (λ b b', r (e.symm b) (e.symm b')) e (λ a₁ a₂, by simp only [e.symm_apply_apply])
id    └────────┘        └┘    └───┘    └───┘ └┘       └┘ └┘
src   └────────┘                    └───┘      └───┘                     └─────────┘                  
typ   └────────┘        └┘    └───┘    └───┘ └┘       └┘ └┘     └─────────┘└────────────────┘
doc   └────────┘                                                         └─────────┘                  
txt                                                                      └─────────┘                  
par                                                                      └─────────┘                  
pid                                                                          └──┘└┘                  
st                                                                      └─────────────────────────────┘
958  
959  end quot
960  
961  namespace quotient
962  /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
963  if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
964  protected def congr {ra : setoid α} {rb : setoid β} (e : α ≃ β)
id                             └────┘         └────┘          
src                            └────┘          └────┘           
typ                            └────┘         └────┘          
doc                                                             
965    (eq : ∀a₁ a₂, @setoid.r α ra a₁ a₂ ↔ @setoid.r β rb (e a₁) (e a₂)) :
id            └┘ └┘   └──────┘  └┘ └┘ └┘   └──────┘  └┘   └┘    └┘
src                   └──────┘              └──────┘
typ           └┘ └┘   └──────┘  └┘ └┘ └┘   └──────┘  └┘   └┘    └┘
966    quotient ra ≃ quotient rb :=
id     └──────┘ └┘  └──────┘ └┘
src    └──────┘     └──────┘
typ    └──────┘ └┘  └──────┘ └┘
doc                
967  quot.congr e eq
id   └────────┘  └┘
src  └────────┘   └┘
typ  └────────┘  └┘
doc  └────────┘
968  
969  /-- Quotients are congruent on equivalences under equality of their relation.
970  An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
971  protected def congr_right {r r' : setoid α}
id                                     └────┘ 
src                                    └────┘
typ                                    └────┘ 
972    (eq : ∀a₁ a₂, @setoid.r α r a₁ a₂ ↔ @setoid.r α r' a₁ a₂) : quotient r ≃ quotient r' :=
id            └┘ └┘   └──────┘   └┘ └┘   └──────┘  └┘ └┘ └┘    └──────┘   └──────┘ └┘
src                   └──────┘             └──────┘               └──────┘    └──────┘
typ           └┘ └┘   └──────┘   └┘ └┘   └──────┘  └┘ └┘ └┘    └──────┘   └──────┘ └┘
doc                                                                           
973  quot.congr_right eq
id   └──────────────┘ └┘
src  └──────────────┘ └┘
typ  └──────────────┘ └┘
doc  └──────────────┘
974  end quotient